diff options
Diffstat (limited to 'mltt/core/lib.ML')
| -rw-r--r-- | mltt/core/lib.ML | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mltt/core/lib.ML b/mltt/core/lib.ML index 98d83cc..6949de6 100644 --- a/mltt/core/lib.ML +++ b/mltt/core/lib.ML @@ -113,9 +113,10 @@ fun decompose_goal ctxt goal = let val focus = #1 (Subgoal.focus_prems ctxt 1 NONE (Thm.trivial (Thm.cterm_of ctxt goal))) - val schematics = #2 (#schematics focus) - |> map (fn (v, ctm) => (Thm.term_of ctm, Var v)) + |> Vars.map (fn v => fn ctm => (Thm.term_of ctm, Var v)) + |> Vars.dest + |> map snd in map Thm.prop_of (#prems focus) @ [Thm.term_of (#concl focus)] |> map (subst_free schematics) |