# HG changeset patch
# User wenzelm
# Date 1631471054 -7200
# Node ID ffe269e74bdd3c17215c44d4857aa28412c901b6
# Parent  33f13d2d211c3f6c775c06ae347dee08cac1854a
more antiquotations;
more formal use of consts;

diff -r 33f13d2d211c -r ffe269e74bdd src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sun Sep 12 20:14:09 2021 +0200
+++ b/src/FOLP/IFOLP.thy	Sun Sep 12 20:24:14 2021 +0200
@@ -63,7 +63,7 @@
 syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
 
 parse_translation \<open>
-  let fun proof_tr [p, P] = Const (\<^const_syntax>\<open>Proof\<close>, dummyT) $ P $ p
+  let fun proof_tr [p, P] = Syntax.const \<^const_syntax>\<open>Proof\<close> $ P $ p
   in [(\<^syntax_const>\<open>_Proof\<close>, K proof_tr)] end
 \<close>
 
@@ -73,7 +73,7 @@
 print_translation \<open>
   let
     fun proof_tr' ctxt [P, p] =
-      if Config.get ctxt show_proofs then Const (\<^syntax_const>\<open>_Proof\<close>, dummyT) $ p $ P
+      if Config.get ctxt show_proofs then Syntax.const \<^syntax_const>\<open>_Proof\<close> $ p $ P
       else P
   in [(\<^const_syntax>\<open>Proof\<close>, proof_tr')] end
 \<close>
@@ -251,7 +251,7 @@
 
 ML \<open>
 local
-  fun discard_proof (Const (\<^const_name>\<open>Proof\<close>, _) $ P $ _) = P;
+  fun discard_proof \<^Const_>\<open>Proof for P _\<close> = P;
 in
 fun uniq_assume_tac ctxt =
   SUBGOAL
@@ -612,8 +612,7 @@
 structure Hypsubst = Hypsubst
 (
   (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const (\<^const_name>\<open>Proof\<close>, _) $
-    (Const (\<^const_name>\<open>eq\<close>, _)  $ t $ u) $ _) = (t, u);
+  fun dest_eq \<^Const_>\<open>Proof for \<open>\<^Const_>\<open>eq _ for t u\<close>\<close> _\<close> = (t, u);
 
   val imp_intr = @{thm impI}
 
diff -r 33f13d2d211c -r ffe269e74bdd src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Sun Sep 12 20:14:09 2021 +0200
+++ b/src/FOLP/hypsubst.ML	Sun Sep 12 20:24:14 2021 +0200
@@ -58,8 +58,8 @@
    assumption.  Returns the number of intervening assumptions, paried with
    the rule asm_rl (resp. sym). *)
 fun eq_var bnd =
-  let fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) = eq_var_aux k t
-        | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) =
+  let fun eq_var_aux k \<^Const_>\<open>Pure.all _ for \<open>Abs(_,_,t)\<close>\<close> = eq_var_aux k t
+        | eq_var_aux k \<^Const_>\<open>Pure.imp for A B\<close> =
               ((k, inspect_pair bnd (dest_eq A))
                       (*Exception Match comes from inspect_pair or dest_eq*)
                handle Match => eq_var_aux (k+1) B)
diff -r 33f13d2d211c -r ffe269e74bdd src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sun Sep 12 20:14:09 2021 +0200
+++ b/src/FOLP/simp.ML	Sun Sep 12 20:24:14 2021 +0200
@@ -158,7 +158,7 @@
               Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars)
             | _$_ => let val (f,args) = strip_comb tm
                      in case f of
-                            Const(c,T) =>
+                            Const(c,_) =>
                                 if member (op =) ccs c
                                 then fold_rev add_hvars args hvars
                                 else Misc_Legacy.add_term_vars (tm, hvars)
@@ -178,7 +178,7 @@
         fun add_vars (tm,vars) = case tm of
                   Abs (_,_,body) => add_vars(body,vars)
                 | r$s => (case head_of tm of
-                          Const(c,T) => (case AList.lookup (op =) new_asms c of
+                          Const(c,_) => (case AList.lookup (op =) new_asms c of
                                   NONE => add_vars(r,add_vars(s,vars))
                                 | SOME(al) => add_list(tm,al,vars))
                         | _ => add_vars(r,add_vars(s,vars)))
@@ -399,10 +399,10 @@
     else ();
 
 (* Skip the first n hyps of a goal, and return the rest in generalized form *)
-fun strip_varify(Const(\<^const_name>\<open>Pure.imp\<close>, _) $ H $ B, n, vs) =
+fun strip_varify(\<^Const_>\<open>Pure.imp for H B\<close>, n, vs) =
         if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
         else strip_varify(B,n-1,vs)
-  | strip_varify(Const(\<^const_name>\<open>Pure.all\<close>,_)$Abs(_,T,t), n, vs) =
+  | strip_varify(\<^Const_>\<open>Pure.all _ for \<open>Abs(_,T,t)\<close>\<close>, n, vs) =
         strip_varify(t,n,Var(("?",length vs),T)::vs)
   | strip_varify  _  = [];
 
@@ -515,7 +515,7 @@
 fun exp_app(0,t) = t
   | exp_app(i,t) = exp_app(i-1,t $ Bound (i-1));
 
-fun exp_abs(Type("fun",[T1,T2]),t,i) =
+fun exp_abs(\<^Type>\<open>fun T1 T2\<close>,t,i) =
         Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
   | exp_abs(T,t,i) = exp_app(i,t);
 
diff -r 33f13d2d211c -r ffe269e74bdd src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Sun Sep 12 20:14:09 2021 +0200
+++ b/src/FOLP/simpdata.ML	Sun Sep 12 20:24:14 2021 +0200
@@ -17,9 +17,9 @@
 (* Conversion into rewrite rules *)
 
 fun mk_eq th = case Thm.concl_of th of
-      _ $ (Const (\<^const_name>\<open>iff\<close>, _) $ _ $ _) $ _ => th
-    | _ $ (Const (\<^const_name>\<open>eq\<close>, _) $ _ $ _) $ _ => th
-    | _ $ (Const (\<^const_name>\<open>Not\<close>, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
+      _ $ \<^Const_>\<open>iff for _ _\<close> $ _ => th
+    | _ $ \<^Const_>\<open>eq _ for _ _\<close> $ _ => th
+    | _ $ \<^Const_>\<open>Not for _\<close> $ _ => th RS @{thm not_P_imp_P_iff_F}
     | _ => make_iff_T th;
 
 
@@ -33,7 +33,7 @@
 fun mk_atomize pairs =
   let fun atoms th =
         (case Thm.concl_of th of
-           Const ("Trueprop", _) $ p =>
+           Const ("Trueprop", _) $ p =>  (* FIXME formal const name!? *)
              (case head_of p of
                 Const(a,_) =>
                   (case AList.lookup (op =) pairs a of