# HG changeset patch
# User wenzelm
# Date 1631390532 -7200
# Node ID ee04dc00bf0a9cc5a651b6adabcc5bdf1a333d3d
# Parent  54279cfcf03751e0afc00279a51647e136a12dd8
more antiquotations;

diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Datatype.thy	Sat Sep 11 22:02:12 2021 +0200
@@ -63,7 +63,7 @@
 struct
   val trace = Unsynchronized.ref false;
 
-  fun mk_new ([],[]) = Const(\<^const_name>\<open>True\<close>,FOLogic.oT)
+  fun mk_new ([],[]) = \<^Const>\<open>True\<close>
     | mk_new (largs,rargs) =
         Balanced_Tree.make FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -89,7 +89,7 @@
            if #big_rec_name lcon_info = #big_rec_name rcon_info
                andalso not (null (#free_iffs lcon_info)) then
                if lname = rname then mk_new (largs, rargs)
-               else Const(\<^const_name>\<open>False\<close>,FOLogic.oT)
+               else \<^Const>\<open>False\<close>
            else raise Match
        val _ =
          if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new)
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -187,7 +187,7 @@
 
   (*Find each recursive argument and add a recursive call for it*)
   fun rec_args [] = []
-    | rec_args ((Const(\<^const_name>\<open>mem\<close>,_)$arg$X)::prems) =
+    | rec_args (\<^Const_>\<open>mem for arg X\<close>::prems) =
        (case head_of X of
             Const(a,_) => (*recursive occurrence?*)
                           if member (op =) rec_names a
@@ -310,7 +310,7 @@
    | SOME recursor_def =>
       let
         (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
-        fun subst_rec (Const(\<^const_name>\<open>apply\<close>,_) $ Free _ $ arg) = recursor_tm $ arg
+        fun subst_rec \<^Const_>\<open>apply for \<open>Free _\<close> arg\<close> = recursor_tm $ arg
           | subst_rec tm =
               let val (head, args) = strip_comb tm
               in  list_comb (head, map subst_rec args)  end;
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -70,8 +70,7 @@
 exception Find_tname of string
 
 fun find_tname ctxt var As =
-  let fun mk_pair (Const(\<^const_name>\<open>mem\<close>,_) $ Free (v,_) $ A) =
-             (v, #1 (dest_Const (head_of A)))
+  let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
       val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
       val x =
@@ -99,7 +98,7 @@
       datatype_info thy tn
       |> (if exh then #exhaustion else #induct)
       |> Thm.transfer thy;
-    val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) =
+    val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
         (case Thm.prems_of rule of
              [] => error "induction is not available for this datatype"
            | major::_ => FOLogic.dest_Trueprop major)
@@ -120,15 +119,14 @@
 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   let
     (*analyze the LHS of a case equation to get a constructor*)
-    fun const_of (Const(\<^const_name>\<open>IFOL.eq\<close>, _) $ (_ $ c) $ _) = c
+    fun const_of \<^Const_>\<open>IFOL.eq _ for \<open>_ $ c\<close> _\<close> = c
       | const_of eqn = error ("Ill-formed case equation: " ^
                               Syntax.string_of_term_global thy eqn);
 
     val constructors =
         map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
 
-    val Const (\<^const_name>\<open>mem\<close>, _) $ _ $ data =
-        FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+    val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
 
     val Const(big_rec_name, _) = head_of data;
 
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -99,7 +99,7 @@
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
-  fun dest_tprop (Const(\<^const_name>\<open>Trueprop\<close>,_) $ P) = P
+  fun dest_tprop \<^Const_>\<open>Trueprop for P\<close> = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
                             Syntax.string_of_term ctxt0 Q);
 
@@ -297,8 +297,7 @@
      (*Used to make induction rules;
         ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
         prem is a premise of an intr rule*)
-     fun add_induct_prem ind_alist (prem as Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                      (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X), iprems) =
+     fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
           (case AList.lookup (op aconv) ind_alist X of
                SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -514,7 +513,7 @@
      (*strip quantifier and the implication*)
      val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
 
-     val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (pred_var $ _) = Thm.concl_of induct0
+     val \<^Const_>\<open>Trueprop for \<open>pred_var $ _\<close>\<close> = Thm.concl_of induct0
 
      val induct0 =
        CP.split_rule_var ctxt4
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -115,8 +115,7 @@
             case AList.lookup (op =) eqns cname of
                 NONE => (warning ("no equation for constructor " ^ cname ^
                                   "\nin definition of function " ^ fname);
-                         (Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT),
-                          #2 recursor_pair, Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT)))
+                         (\<^Const>\<open>zero\<close>, #2 recursor_pair, \<^Const>\<open>zero\<close>))
               | SOME (rhs, cargs', eq) =>
                     (rhs, inst_recursor (recursor_pair, cargs'), eq)
           val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/typechk.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -76,8 +76,7 @@
          if length rls <= maxr then resolve_tac ctxt rls i else no_tac
       end);
 
-fun is_rigid_elem (Const(\<^const_name>\<open>Trueprop\<close>,_) $ (Const(\<^const_name>\<open>mem\<close>,_) $ a $ _)) =
-      not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
   | is_rigid_elem _ = false;
 
 (*Try solving a:A by assumption provided a is rigid!*)
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/arith_data.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -24,8 +24,8 @@
 
 val iT = Ind_Syntax.iT;
 
-val zero = Const(\<^const_name>\<open>zero\<close>, iT);
-val succ = Const(\<^const_name>\<open>succ\<close>, iT --> iT);
+val zero = \<^Const>\<open>zero\<close>;
+val succ = \<^Const>\<open>succ\<close>;
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
 
@@ -44,9 +44,9 @@
 
 (* dest_sum *)
 
-fun dest_sum (Const(\<^const_name>\<open>zero\<close>,_)) = []
-  | dest_sum (Const(\<^const_name>\<open>succ\<close>,_) $ t) = one :: dest_sum t
-  | dest_sum (Const(\<^const_name>\<open>Arith.add\<close>,_) $ t $ u) = dest_sum t @ dest_sum u
+fun dest_sum \<^Const_>\<open>zero\<close> = []
+  | dest_sum \<^Const_>\<open>succ for t\<close> = one :: dest_sum t
+  | dest_sum \<^Const_>\<open>Arith.add for t u\<close> = dest_sum t @ dest_sum u
   | dest_sum tm = [tm];
 
 (*Apply the given rewrite (if present) just once*)
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -18,7 +18,7 @@
 
 (** Abstract syntax definitions for ZF **)
 
-val iT = Type(\<^type_name>\<open>i\<close>, []);
+val iT = \<^Type>\<open>i\<close>;
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
@@ -29,17 +29,16 @@
 fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t;
 
 (*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _) =
+fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
         error"Premises may not be conjuctive"
-  | chk_prem rec_hd (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) =
+  | chk_prem rec_hd \<^Const_>\<open>mem for t X\<close> =
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
   | chk_prem rec_hd t =
         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl =
-    let val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) =
-                Logic.strip_imp_concl rl
+    let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)
@@ -61,7 +60,7 @@
 type constructor_spec =
     (string * typ * mixfix) * string * term list * term list;
 
-fun dest_mem (Const (\<^const_name>\<open>mem\<close>, _) $ x $ A) = (x, A)
+fun dest_mem \<^Const_>\<open>mem for x A\<close> = (x, A)
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/int_arith.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -44,7 +44,7 @@
 
 fun mk_numeral i = \<^const>\<open>integ_of\<close> $ mk_bin i;
 
-fun dest_numeral (Const(\<^const_name>\<open>integ_of\<close>, _) $ w) = dest_bin w
+fun dest_numeral \<^Const_>\<open>integ_of for w\<close> = dest_bin w
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun find_first_numeral past (t::terms) =
@@ -65,9 +65,9 @@
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (\<^const_name>\<open>zadd\<close>, _) $ t $ u, ts) =
+fun dest_summing (pos, \<^Const_>\<open>zadd for t u\<close>, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const (\<^const_name>\<open>zdiff\<close>, _) $ t $ u, ts) =
+  | dest_summing (pos, \<^Const_>\<open>zdiff for t u\<close>, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else \<^const>\<open>zminus\<close> $ t :: ts;
@@ -93,7 +93,7 @@
 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (\<^const_name>\<open>zminus\<close>, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign \<^Const_>\<open>zminus for t\<close> = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term_Ord.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
diff -r 54279cfcf037 -r ee04dc00bf0a src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/simpdata.ML	Sat Sep 11 22:02:12 2021 +0200
@@ -19,11 +19,11 @@
                    | NONE => [th])
             | _ => [th]
   in case Thm.concl_of th of
-         Const(\<^const_name>\<open>Trueprop\<close>,_) $ P =>
+         \<^Const_>\<open>Trueprop for P\<close> =>
             (case P of
-                 Const(\<^const_name>\<open>mem\<close>,_) $ a $ b => tryrules mem_pairs b
-               | Const(\<^const_name>\<open>True\<close>,_)         => []
-               | Const(\<^const_name>\<open>False\<close>,_)        => []
+                 \<^Const_>\<open>mem for a b\<close> => tryrules mem_pairs b
+               | \<^Const_>\<open>True\<close> => []
+               | \<^Const_>\<open>False\<close> => []
                | A => tryrules conn_pairs A)
        | _                       => [th]
   end;