# HG changeset patch
# User wenzelm
# Date 1631392081 -7200
# Node ID abc8789732164e9bda2b6ac3897481f95a6a9b99
# Parent  9a9326a072bb296cb4e8d4545ae7cde294cbec7c
clarified antiquotation;

diff -r 9a9326a072bb -r abc878973216 src/ZF/Inductive.thy
--- a/src/ZF/Inductive.thy	Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Inductive.thy	Sat Sep 11 22:28:01 2021 +0200
@@ -37,8 +37,8 @@
 ML \<open>
 structure Lfp =
   struct
-  val oper      = \<^const>\<open>lfp\<close>
-  val bnd_mono  = \<^const>\<open>bnd_mono\<close>
+  val oper      = \<^Const>\<open>lfp\<close>
+  val bnd_mono  = \<^Const>\<open>bnd_mono\<close>
   val bnd_monoI = @{thm bnd_monoI}
   val subs      = @{thm def_lfp_subset}
   val Tarski    = @{thm def_lfp_unfold}
@@ -47,8 +47,8 @@
 
 structure Standard_Prod =
   struct
-  val sigma     = \<^const>\<open>Sigma\<close>
-  val pair      = \<^const>\<open>Pair\<close>
+  val sigma     = \<^Const>\<open>Sigma\<close>
+  val pair      = \<^Const>\<open>Pair\<close>
   val split_name = \<^const_name>\<open>split\<close>
   val pair_iff  = @{thm Pair_iff}
   val split_eq  = @{thm split}
@@ -61,10 +61,10 @@
 
 structure Standard_Sum =
   struct
-  val sum       = \<^const>\<open>sum\<close>
-  val inl       = \<^const>\<open>Inl\<close>
-  val inr       = \<^const>\<open>Inr\<close>
-  val elim      = \<^const>\<open>case\<close>
+  val sum       = \<^Const>\<open>sum\<close>
+  val inl       = \<^Const>\<open>Inl\<close>
+  val inr       = \<^Const>\<open>Inr\<close>
+  val elim      = \<^Const>\<open>case\<close>
   val case_inl  = @{thm case_Inl}
   val case_inr  = @{thm case_Inr}
   val inl_iff   = @{thm Inl_iff}
@@ -84,8 +84,8 @@
 
 structure Gfp =
   struct
-  val oper      = \<^const>\<open>gfp\<close>
-  val bnd_mono  = \<^const>\<open>bnd_mono\<close>
+  val oper      = \<^Const>\<open>gfp\<close>
+  val bnd_mono  = \<^Const>\<open>bnd_mono\<close>
   val bnd_monoI = @{thm bnd_monoI}
   val subs      = @{thm def_gfp_subset}
   val Tarski    = @{thm def_gfp_unfold}
@@ -94,8 +94,8 @@
 
 structure Quine_Prod =
   struct
-  val sigma     = \<^const>\<open>QSigma\<close>
-  val pair      = \<^const>\<open>QPair\<close>
+  val sigma     = \<^Const>\<open>QSigma\<close>
+  val pair      = \<^Const>\<open>QPair\<close>
   val split_name = \<^const_name>\<open>qsplit\<close>
   val pair_iff  = @{thm QPair_iff}
   val split_eq  = @{thm qsplit}
@@ -108,10 +108,10 @@
 
 structure Quine_Sum =
   struct
-  val sum       = \<^const>\<open>qsum\<close>
-  val inl       = \<^const>\<open>QInl\<close>
-  val inr       = \<^const>\<open>QInr\<close>
-  val elim      = \<^const>\<open>qcase\<close>
+  val sum       = \<^Const>\<open>qsum\<close>
+  val inl       = \<^Const>\<open>QInl\<close>
+  val inr       = \<^Const>\<open>QInr\<close>
+  val elim      = \<^Const>\<open>qcase\<close>
   val case_inl  = @{thm qcase_QInl}
   val case_inr  = @{thm qcase_QInr}
   val inl_iff   = @{thm QInl_iff}
diff -r 9a9326a072bb -r abc878973216 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Sep 11 22:28:01 2021 +0200
@@ -56,7 +56,7 @@
                    Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t));
         val rec_names = (*nat doesn't have to be added*)
             \<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds
-        val u = if co then \<^const>\<open>QUniv.quniv\<close> else \<^const>\<open>Univ.univ\<close>
+        val u = if co then \<^Const>\<open>QUniv.quniv\<close> else \<^Const>\<open>Univ.univ\<close>
         val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
           (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
             | _ => I)) con_ty_lists [];
@@ -88,7 +88,7 @@
   (** Define the constructors **)
 
   (*The empty tuple is 0*)
-  fun mk_tuple [] = \<^const>\<open>zero\<close>
+  fun mk_tuple [] = \<^Const>\<open>zero\<close>
     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
 
   fun mk_inject n k u = Balanced_Tree.access
@@ -162,7 +162,7 @@
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
 
   (*a recursive call for x is the application rec`x  *)
-  val rec_call = \<^const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
+  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
 
   (*look back down the "case args" (which have been reversed) to
     determine the de Bruijn index*)
@@ -231,7 +231,7 @@
   val recursor_def =
       Misc_Legacy.mk_defpair
         (recursor_tm,
-         \<^const>\<open>Univ.Vrecursor\<close> $
+         \<^Const>\<open>Univ.Vrecursor\<close> $
            absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
diff -r 9a9326a072bb -r abc878973216 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sat Sep 11 22:28:01 2021 +0200
@@ -115,7 +115,7 @@
 
   (*The Part(A,h) terms -- compose injections to make h*)
   fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
-    | mk_Part h = \<^const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
+    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
 
   (*Access to balanced disjoint sums via injections*)
   val parts = map mk_Part
@@ -302,7 +302,7 @@
                SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
                  let fun mk_sb (rec_tm,pred) =
-                             (rec_tm, \<^const>\<open>Collect\<close> $ rec_tm $ pred)
+                             (rec_tm, \<^Const>\<open>Collect\<close> $ rec_tm $ pred)
                  in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
        | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
 
@@ -390,8 +390,7 @@
                             elem_factors ---> FOLogic.oT)
            val qconcl =
              List.foldr FOLogic.mk_all
-               (FOLogic.imp $
-                (\<^const>\<open>mem\<close> $ elem_tuple $ rec_tm)
+               (FOLogic.imp $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
                       $ (list_comb (pfree, elem_frees))) elem_frees
        in  (CP.ap_split elem_type FOLogic.oT pfree,
             qconcl)
@@ -401,8 +400,7 @@
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         FOLogic.imp $ (\<^const>\<open>mem\<close> $ Bound 0 $ rec_tm) $
-                          (pred $ Bound 0);
+         FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
 
      (*To instantiate the main induction rule*)
      val induct_concl =
diff -r 9a9326a072bb -r abc878973216 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Sat Sep 11 22:28:01 2021 +0200
@@ -23,10 +23,9 @@
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
     FOLogic.all_const iT $
-      Abs("v", iT, FOLogic.imp $ (\<^const>\<open>mem\<close> $ Bound 0 $ A) $
-                   Term.betapply(P, Bound 0));
+      Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
 
-fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
@@ -82,20 +81,19 @@
       Logic.list_implies
         (map FOLogic.mk_Trueprop prems,
          FOLogic.mk_Trueprop
-            (\<^const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args)
-                       $ rec_tm))
+            (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
 
-fun mk_Un (t1, t2) = \<^const>\<open>Un\<close> $ t1 $ t2;
+fun mk_Un (t1, t2) = \<^Const>\<open>Un for t1 t2\<close>;
 
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = iT)
   in  case filter is_ind (args @ cs) of
-         [] => \<^const>\<open>zero\<close>
+         [] => \<^Const>\<open>zero\<close>
        | u_args => Balanced_Tree.make mk_Un u_args
   end;
 
diff -r 9a9326a072bb -r abc878973216 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/int_arith.ML	Sat Sep 11 22:28:01 2021 +0200
@@ -42,7 +42,7 @@
 
 (*Utilities*)
 
-fun mk_numeral i = \<^const>\<open>integ_of\<close> $ mk_bin i;
+fun mk_numeral i = \<^Const>\<open>integ_of\<close> $ mk_bin i;
 
 fun dest_numeral \<^Const_>\<open>integ_of for w\<close> = dest_bin w
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
@@ -70,7 +70,7 @@
   | 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;
+        if pos then t::ts else \<^Const>\<open>zminus for t\<close> :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);