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.

5 files changed, 20 insertions, 12 deletions

diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index 96cbe96..ec923e2 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -25,11 +25,11 @@ let
   val typ = Simple_Syntax.read_typ
   fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
 in
-  Sign.del_syntax (Print_Mode.ASCII, true)
+  Sign.syntax false (Print_Mode.ASCII, true)
     [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3))]
-  #> Sign.del_syntax Syntax.mode_default
+  #> Sign.syntax false Syntax.mode_default
     [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))]
-  #> Sign.add_syntax Syntax.mode_default
+  #> Sign.syntax true Syntax.mode_default
     [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))]
 end
 \<close>
@@ -309,10 +309,16 @@ subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)
 method_setup this =
   \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts =>
     CHEADGOAL (SIDE_CONDS 0
-      (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
+      (CONTEXT_TACTIC' (fn ctxt => simp_tac (ctxt addsimps facts)))
       facts))))\<close>
 
 
+method_setup infer =
+  \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts =>
+    CHEADGOAL (SIDE_CONDS 0
+      (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
+      facts))))\<close>
+
 subsection \<open>Rewriting\<close>
 
 consts compute_hole :: "'a::{}"  ("\<hole>")
@@ -564,5 +570,4 @@ Lemma (def) distribute_Sig:
       by typechk+
   qed
 
-
 end
diff --git a/mltt/core/comp.ML b/mltt/core/comp.ML
index 2e50753..8725ba3 100644
--- a/mltt/core/comp.ML
+++ b/mltt/core/comp.ML
@@ -279,7 +279,7 @@ fun comps_pconv to thms ctxt (tyenv, env_ts) =
               ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
         val tyinsts = Term.add_tvars prop []
           |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
-      in Drule.instantiate_normalize (tyinsts, insts) thm end
+      in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end
     
     fun unify_with_rhs context to env thm =
       let
diff --git a/mltt/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML
index 33f88cf..2e129c8 100644
--- a/mltt/core/elaborated_statement.ML
+++ b/mltt/core/elaborated_statement.ML
@@ -95,12 +95,14 @@ fun inst_morphism params ((prfx, mandatory), insts') ctxt =
     (*instantiation*)
     val instT =
       (type_parms ~~ map Logic.dest_type type_parms'')
-      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
+      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T))
+      |> TFrees.make;
     val cert_inst =
       ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
-      |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
+      |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t))
+      |> Frees.make;
   in
-    (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
+    (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $>
       Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;
 
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'
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)