more antiquotations;
more formal use of consts;

--- a/src/Sequents/Modal0.thy	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/Modal0.thy	Sun Sep 12 20:37:15 2021 +0200
@@ -20,8 +20,8 @@
   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
 ML \<open>
-  fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
-  fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
+  fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2;
+  fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
 \<close>
 
 parse_translation \<open>

--- a/src/Sequents/S43.thy	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/S43.thy	Sun Sep 12 20:37:15 2021 +0200
@@ -20,7 +20,7 @@
   let
     val tr  = seq_tr;
     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
-      Const (\<^const_syntax>\<open>S43pi\<close>, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
+      Syntax.const \<^const_syntax>\<open>S43pi\<close> $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
   in [(\<^syntax_const>\<open>_S43pi\<close>, K s43pi_tr)] end
 \<close>
 
@@ -28,7 +28,7 @@
 let
   val tr' = seq_tr';
   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
-    Const(\<^syntax_const>\<open>_S43pi\<close>, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
+    Syntax.const \<^syntax_const>\<open>_S43pi\<close> $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
 in [(\<^const_syntax>\<open>S43pi\<close>, K s43pi_tr')] end
 \<close>
 

--- a/src/Sequents/Sequents.thy	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/Sequents.thy	Sun Sep 12 20:37:15 2021 +0200
@@ -58,10 +58,9 @@
 
 (* parse translation for sequences *)
 
-fun abs_seq' t = Abs ("s", Type (\<^type_name>\<open>seq'\<close>, []), t);
+fun abs_seq' t = Abs ("s", \<^Type>\<open>seq'\<close>, t);
 
-fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) =
-      Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f
+fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) = Syntax.const \<^const_syntax>\<open>SeqO'\<close> $ f
   | seqobj_tr (_ $ i) = i;
 
 fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0
@@ -73,29 +72,28 @@
       abs_seq'(seqobj_tr so $ seqcont_tr sc);
 
 fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) =
-  abs_seq' ((Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f) $ Bound 0);
+  abs_seq' ((Syntax.const \<^const_syntax>\<open>SeqO'\<close> $ f) $ Bound 0);
 
 
 (* print translation for sequences *)
 
-fun seqcont_tr' (Bound 0) =
-      Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT)
+fun seqcont_tr' (Bound 0) = Syntax.const \<^syntax_const>\<open>_SeqContEmp\<close>
   | seqcont_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
-      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
-        (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
+      Syntax.const \<^syntax_const>\<open>_SeqContApp\<close> $
+        (Syntax.const \<^syntax_const>\<open>_SeqO\<close> $ f) $ seqcont_tr' s
   | seqcont_tr' (i $ s) =
-      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
-        (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s;
+      Syntax.const \<^syntax_const>\<open>_SeqContApp\<close> $
+        (Syntax.const \<^syntax_const>\<open>_SeqId\<close> $ i) $ seqcont_tr' s;
 
 fun seq_tr' s =
   let
-    fun seq_itr' (Bound 0) = Const (\<^syntax_const>\<open>_SeqEmp\<close>, dummyT)
+    fun seq_itr' (Bound 0) = Syntax.const \<^syntax_const>\<open>_SeqEmp\<close>
       | seq_itr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
-          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
-            (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
+          Syntax.const \<^syntax_const>\<open>_SeqApp\<close> $
+            (Syntax.const \<^syntax_const>\<open>_SeqO\<close> $ f) $ seqcont_tr' s
       | seq_itr' (i $ s) =
-          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
-            (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s
+          Syntax.const \<^syntax_const>\<open>_SeqApp\<close> $
+            (Syntax.const \<^syntax_const>\<open>_SeqId\<close> $ i) $ seqcont_tr' s
   in
     case s of
       Abs (_, _, t) => seq_itr' t
@@ -104,33 +102,33 @@
 
 
 fun single_tr c [s1, s2] =
-  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
+  Syntax.const c $ seq_tr s1 $ singlobj_tr s2;
 
 fun two_seq_tr c [s1, s2] =
-  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
+  Syntax.const c $ seq_tr s1 $ seq_tr s2;
 
 fun three_seq_tr c [s1, s2, s3] =
-  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
+  Syntax.const c $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
 
 fun four_seq_tr c [s1, s2, s3, s4] =
-  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
+  Syntax.const c $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
 
 
 fun singlobj_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>,_) $ fm) = fm
-  | singlobj_tr' id = Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ id;
+  | singlobj_tr' id = Syntax.const \<^syntax_const>\<open>_SeqId\<close> $ id;
 
 
 fun single_tr' c [s1, s2] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
+  Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
 
 fun two_seq_tr' c [s1, s2] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
+  Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
 
 fun three_seq_tr' c [s1, s2, s3] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
+  Syntax.const c $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
 
 fun four_seq_tr' c [s1, s2, s3, s4] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
+  Syntax.const c $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
 
 
 

--- a/src/Sequents/modal.ML	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/modal.ML	Sun Sep 12 20:37:15 2021 +0200
@@ -26,7 +26,7 @@
 struct
 
 (*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq \<^Const_>\<open>SeqO' for P u\<close> = P :: forms_of_seq u
   | forms_of_seq (H $ u) = forms_of_seq u
   | forms_of_seq _ = [];
 

--- a/src/Sequents/prover.ML	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/prover.ML	Sun Sep 12 20:37:15 2021 +0200
@@ -117,7 +117,7 @@
 
 
 (*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq \<^Const_>\<open>SeqO' for P u\<close> = P :: forms_of_seq u
   | forms_of_seq (H $ u) = forms_of_seq u
   | forms_of_seq _ = [];
 

--- a/src/Sequents/simpdata.ML	Sun Sep 12 20:24:14 2021 +0200
+++ b/src/Sequents/simpdata.ML	Sun Sep 12 20:37:15 2021 +0200
@@ -13,30 +13,30 @@
 (*Make atomic rewrite rules*)
 fun atomize r =
  case Thm.concl_of r of
-   Const(\<^const_name>\<open>Trueprop\<close>,_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+   \<^Const_>\<open>Trueprop for \<open>Abs(_,_,a)\<close> \<open>Abs(_,_,c)\<close>\<close> =>
      (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
         ([], [p]) =>
           (case p of
-               Const(\<^const_name>\<open>imp\<close>,_)$_$_ => atomize(r RS @{thm mp_R})
-             | Const(\<^const_name>\<open>conj\<close>,_)$_$_   => atomize(r RS @{thm conjunct1}) @
+               \<^Const_>\<open>imp for _ _\<close> => atomize(r RS @{thm mp_R})
+             | \<^Const_>\<open>conj for _ _\<close> => atomize(r RS @{thm conjunct1}) @
                    atomize(r RS @{thm conjunct2})
-             | Const(\<^const_name>\<open>All\<close>,_)$_      => atomize(r RS @{thm spec})
-             | Const(\<^const_name>\<open>True\<close>,_)       => []    (*True is DELETED*)
-             | Const(\<^const_name>\<open>False\<close>,_)      => []    (*should False do something?*)
+             | \<^Const_>\<open>All _ for _\<close> => atomize(r RS @{thm spec})
+             | \<^Const_>\<open>True\<close> => []    (*True is DELETED*)
+             | \<^Const_>\<open>False\<close> => []    (*should False do something?*)
              | _                     => [r])
       | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
  | _ => [r];
 
 (*Make meta-equalities.*)
 fun mk_meta_eq ctxt th = case Thm.concl_of th of
-    Const(\<^const_name>\<open>Pure.eq\<close>,_)$_$_ => th
-  | Const(\<^const_name>\<open>Trueprop\<close>,_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+    \<^Const_>\<open>Pure.eq _ for _ _\<close> => th
+  | \<^Const_>\<open>Trueprop for \<open>Abs(_,_,a)\<close> \<open>Abs(_,_,c)\<close>\<close> =>
         (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
              ([], [p]) =>
                  (case p of
-                      (Const(\<^const_name>\<open>equal\<close>,_)$_$_)   => th RS @{thm eq_reflection}
-                    | (Const(\<^const_name>\<open>iff\<close>,_)$_$_) => th RS @{thm iff_reflection}
-                    | (Const(\<^const_name>\<open>Not\<close>,_)$_)      => th RS @{thm iff_reflection_F}
+                      \<^Const_>\<open>equal _ for _ _\<close> => th RS @{thm eq_reflection}
+                    | \<^Const_>\<open>iff for _ _\<close> => th RS @{thm iff_reflection}
+                    | \<^Const_>\<open>Not for _\<close> => th RS @{thm iff_reflection_F}
                     | _                       => th RS @{thm iff_reflection_T})
            | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));