From cb4139dc35527bd8c8f9b70753c3d1f552c5f19d Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Wed, 29 Jun 2022 01:14:51 +0200
Subject: make mltt work with isabelle 2021-1

notably, this modifies the proof method `this`: the previous version
of it no longer works with cconv.ML (borrowed from HOL), so now it's
just a call to the simplifier, which does work.

Unfortunately the new `this` can otherwise do less than the old one
(it does not instantiate schematic variables), so the old one is now
available as `infer` instead.
---
 mltt/core/lib.ML | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'mltt/core/lib.ML')

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)
-- 
cgit v1.2.3