diff options
Diffstat (limited to 'mltt/core/focus.ML')
| -rw-r--r-- | mltt/core/focus.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mltt/core/focus.ML b/mltt/core/focus.ML index b963cfe..ac4de08 100644 --- a/mltt/core/focus.ML +++ b/mltt/core/focus.ML @@ -36,7 +36,7 @@ fun gen_focus ctxt i bindings raw_st = |> apfst rev |> apsnd reverse_prems val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2 - val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst) + val schematic_terms = Vars.map (fn _ => fn b => Thm.cterm_of ctxt3 b) (#2 inst) val schematics = (schematic_types, schematic_terms) val asms' = map (Thm.instantiate_cterm schematics) asms' val concl' = Thm.instantiate_cterm schematics concl' |