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.

1 files changed, 10 insertions, 5 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