clarified antiquotations;

--- a/src/HOL/HOL.thy	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 28 22:14:44 2021 +0200
@@ -888,7 +888,7 @@
   structure Blast = Blast
   (
     structure Classical = Classical
-    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
+    val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close>
     val equality_name = \<^const_name>\<open>HOL.eq\<close>
     val not_name = \<^const_name>\<open>Not\<close>
     val notE = @{thm notE}
@@ -1549,7 +1549,7 @@
         {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
          proc = fn _ => fn _ => fn ct =>
           (case Thm.term_of ct of
-            _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
+            _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
               if P <> Q then SOME Drule.swap_prems_eq else NONE
           | _ => NONE)},
        Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
@@ -1558,11 +1558,11 @@
           (case Thm.term_of ct of
             _ $ (_ $ P) $ _ =>
               let
-                fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) =
+                fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> =
                       is_conj P andalso is_conj Q
-                  | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true
-                  | is_conj \<^const>\<open>induct_true\<close> = true
-                  | is_conj \<^const>\<open>induct_false\<close> = true
+                  | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
+                  | is_conj \<^Const_>\<open>induct_true\<close> = true
+                  | is_conj \<^Const_>\<open>induct_false\<close> = true
                   | is_conj _ = false
               in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
             | _ => NONE)}]

--- a/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 22:14:44 2021 +0200
@@ -97,7 +97,7 @@
 
 fun check_pattern_syntax t =
   case strip_all t of
-    (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+    (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
       let
         fun go (Const (\<^const_name>\<open>as\<close>, _) $ pat $ var, rhs) =
               let
@@ -126,7 +126,7 @@
 
 fun uncheck_pattern_syntax ctxt t =
   case strip_all t of
-    (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+    (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
       let
         (* restricted to going down abstractions; ignores eta-contracted rhs *)
         fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ pat $ Abs (name, typ, t)) ctxt frees =

--- a/src/HOL/Library/code_lazy.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -378,8 +378,8 @@
       ||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
 
     val mk_Lazy_delay_eq =
-      (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^const>\<open>Unity\<close>))
-      |> mk_eq |> all_abs [\<^typ>\<open>unit\<close> --> lazy_type]
+      (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^Const>\<open>Unity\<close>))
+      |> mk_eq |> all_abs [\<^Type>\<open>unit\<close> --> lazy_type]
     val (Lazy_delay_thm, lthy8a) = mk_thm 
       ((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
       lthy8

--- a/src/HOL/Library/code_test.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/code_test.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -179,15 +179,15 @@
       lhs :: rhs :: acc)
   | add_eval _ = I
 
-fun mk_term_of [] = \<^term>\<open>None :: (unit \<Rightarrow> yxml_of_term) option\<close>
+fun mk_term_of [] = \<^Const>\<open>None \<^typ>\<open>unit \<Rightarrow> yxml_of_term\<close>\<close>
   | mk_term_of ts =
       let
         val tuple = mk_tuples ts
         val T = fastype_of tuple
       in
         \<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $
-          (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $
-            (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple)))
+          (absdummy \<^typ>\<open>unit\<close> (\<^Const>\<open>yxml_string_of_term\<close> $
+            (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^Type>\<open>term\<close>) $ tuple)))
       end
 
 fun test_terms ctxt ts target =

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -303,11 +303,11 @@
 
 fun name_of_disc t =
   (case head_of t of
-    Abs (_, _, \<^const>\<open>Not\<close> $ (t' $ Bound 0)) =>
+    Abs (_, _, \<^Const_>\<open>Not for \<open>t' $ Bound 0\<close>\<close>) =>
     Long_Name.map_base_name (prefix not_prefix) (name_of_disc t')
-  | Abs (_, _, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t') =>
+  | Abs (_, _, \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>) =>
     Long_Name.map_base_name (prefix is_prefix) (name_of_disc t')
-  | Abs (_, _, \<^const>\<open>Not\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t')) =>
+  | Abs (_, _, \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>\<close>) =>
     Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t')
   | t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
 
@@ -1037,7 +1037,7 @@
 
               val disc_eq_case_thms =
                 let
-                  fun const_of_bool b = if b then \<^const>\<open>True\<close> else \<^const>\<open>False\<close>;
+                  fun const_of_bool b = if b then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>;
                   fun mk_case_args n = map_index (fn (k, argTs) =>
                     fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss;
                   val goals = map_index (fn (n, udisc) =>

--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -400,7 +400,7 @@
       let val (sel_rhs, wits) = mk_sel_case_args lthy4 ctr_Tss ks arg
       in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
     fun mk_dis_case_args args k  = map (fn (k', arg) => (if k = k'
-      then fold_rev Term.lambda arg \<^const>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) args;
+      then fold_rev Term.lambda arg \<^Const>\<open>True\<close> else fold_rev Term.lambda arg \<^Const>\<open>False\<close>)) args;
     val sel_rhs = map (map mk_sel_rhs) sel_argss
     val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
     val dis_qty = qty_isom --> HOLogic.boolT;

--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -131,7 +131,7 @@
 
 fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
 
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
   | has_lonely_bool_var _ = false;
 
 val syntactic_sorts =

--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -240,7 +240,7 @@
 
 fun mutual_co_datatypes_of ctxt (T_name, Ts) =
   (if T_name = \<^type_name>\<open>itself\<close> then
-     (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[@{const Pure.type ('a)}]])
+     (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[\<^Const>\<open>Pure.type \<^typ>\<open>'a\<close>\<close>]])
    else
      let
        val (fp, ctr_sugars) =
@@ -269,7 +269,7 @@
       val A = Logic.varifyT_global \<^typ>\<open>'a\<close>;
       val absT = Type (\<^type_name>\<open>set\<close>, [A]);
       val repT = A --> HOLogic.boolT;
-      val pred = Abs (Name.uu, repT, \<^const>\<open>True\<close>);
+      val pred = Abs (Name.uu, repT, \<^Const>\<open>True\<close>);
       val abs = Const (\<^const_name>\<open>Collect\<close>, repT --> absT);
       val rep = Const (\<^const_name>\<open>rmember\<close>, absT --> repT);
     in
@@ -518,8 +518,8 @@
     fold process_spec specs NONE
   end;
 
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
-  | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+  | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
 
 fun specialize_definition_type thy x def0 =
   let
@@ -674,10 +674,10 @@
         [cmd] :: (group :: groups)
     end;
 
-fun defined_by (Const (\<^const_name>\<open>All\<close>, _) $ t) = defined_by t
+fun defined_by \<^Const_>\<open>All _ for t\<close> = defined_by t
   | defined_by (Abs (_, _, t)) = defined_by t
-  | defined_by (\<^const>\<open>implies\<close> $ _ $ u) = defined_by u
-  | defined_by (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) = head_of t
+  | defined_by \<^Const_>\<open>implies for _ u\<close> = defined_by u
+  | defined_by \<^Const_>\<open>HOL.eq _ for t _\<close> = head_of t
   | defined_by t = head_of t;
 
 fun partition_props [_] props = SOME [props]
@@ -1002,14 +1002,14 @@
     val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt
       |> List.partition has_polymorphism;
 
-    fun implicit_evals_of pol (\<^const>\<open>Not\<close> $ t) = implicit_evals_of (not pol) t
-      | implicit_evals_of pol (\<^const>\<open>implies\<close> $ t $ u) =
+    fun implicit_evals_of pol \<^Const_>\<open>Not for t\<close> = implicit_evals_of (not pol) t
+      | implicit_evals_of pol \<^Const_>\<open>implies for t u\<close> =
         (case implicit_evals_of pol u of
           [] => implicit_evals_of (not pol) t
         | ts => ts)
-      | implicit_evals_of pol (\<^const>\<open>conj\<close> $ t $ u) =
+      | implicit_evals_of pol \<^Const_>\<open>conj for t u\<close> =
         union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
-      | implicit_evals_of pol (\<^const>\<open>disj\<close> $ t $ u) =
+      | implicit_evals_of pol \<^Const_>\<open>disj for t u\<close> =
         union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
       | implicit_evals_of false (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) =
         distinct (op aconv) [t, u]
@@ -1049,7 +1049,7 @@
   Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t);
 
 fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body
-  | is_triv_wrt \<^const>\<open>True\<close> = true
+  | is_triv_wrt \<^Const>\<open>True\<close> = true
   | is_triv_wrt _ = false;
 
 fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} =

--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -166,11 +166,11 @@
         else if id = nun_equals then
           Const (\<^const_name>\<open>HOL.eq\<close>, typ_of ty)
         else if id = nun_false then
-          \<^const>\<open>False\<close>
+          \<^Const>\<open>False\<close>
         else if id = nun_if then
           Const (\<^const_name>\<open>If\<close>, typ_of ty)
         else if id = nun_implies then
-          \<^term>\<open>implies\<close>
+          \<^Const>\<open>implies\<close>
         else if id = nun_not then
           HOLogic.Not
         else if id = nun_unique then
@@ -178,7 +178,7 @@
         else if id = nun_unique_unsafe then
           Const (\<^const_name>\<open>The_unsafe\<close>, typ_of ty)
         else if id = nun_true then
-          \<^const>\<open>True\<close>
+          \<^Const>\<open>True\<close>
         else if String.isPrefix nun_dollar_anon_fun_prefix id then
           let val j = Int.fromString (unprefix nun_dollar_anon_fun_prefix id) |> the_default ~1 in
             Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
@@ -225,12 +225,12 @@
         end
       | term_of _ (NMatch _) = raise Fail "unexpected match";
 
-    fun rewrite_numbers (t as \<^const>\<open>Suc\<close> $ _) =
+    fun rewrite_numbers (t as \<^Const>\<open>Suc\<close> $ _) =
         (case try HOLogic.dest_nat t of
-          SOME n => HOLogic.mk_number \<^typ>\<open>nat\<close> n
+          SOME n => HOLogic.mk_number \<^Type>\<open>nat\<close> n
         | NONE => t)
-      | rewrite_numbers (\<^const>\<open>Abs_Integ\<close> $ (@{const Pair (nat, nat)} $ t $ u)) =
-        HOLogic.mk_number \<^typ>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
+      | rewrite_numbers \<^Const_>\<open>Abs_Integ for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t u\<close>\<close> =
+        HOLogic.mk_number \<^Type>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
       | rewrite_numbers (t $ u) = rewrite_numbers t $ rewrite_numbers u
       | rewrite_numbers (Abs (s, T, t)) = Abs (s, T, rewrite_numbers t)
       | rewrite_numbers t = t;

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -466,8 +466,8 @@
 fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
 
 fun make_set T1 [] = Const (\<^const_abbrev>\<open>Set.empty\<close>, T1 --> \<^typ>\<open>bool\<close>)
-  | make_set T1 ((_, \<^const>\<open>False\<close>) :: tps) = make_set T1 tps
-  | make_set T1 ((t1, \<^const>\<open>True\<close>) :: tps) =
+  | make_set T1 ((_, \<^Const_>\<open>False\<close>) :: tps) = make_set T1 tps
+  | make_set T1 ((t1, \<^Const_>\<open>True\<close>) :: tps) =
       Const (\<^const_name>\<open>insert\<close>, T1 --> (T1 --> \<^typ>\<open>bool\<close>) --> T1 --> \<^typ>\<open>bool\<close>) $
         t1 $ (make_set T1 tps)
   | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
@@ -476,8 +476,8 @@
   | make_coset T tps =
     let
       val U = T --> \<^typ>\<open>bool\<close>
-      fun invert \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
-        | invert \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
+      fun invert \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+        | invert \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
     in
       Const (\<^const_name>\<open>Groups.minus_class.minus\<close>, U --> U --> U) $
         Const (\<^const_abbrev>\<open>UNIV\<close>, U) $ make_set T (map (apsnd invert) tps)
@@ -505,8 +505,8 @@
               (case T2 of
                 \<^typ>\<open>bool\<close> =>
                   (case t of
-                     Abs(_, _, \<^const>\<open>False\<close>) => fst #> rev #> make_set T1
-                   | Abs(_, _, \<^const>\<open>True\<close>) => fst #> rev #> make_coset T1
+                     Abs(_, _, \<^Const_>\<open>False\<close>) => fst #> rev #> make_set T1
+                   | Abs(_, _, \<^Const_>\<open>True\<close>) => fst #> rev #> make_coset T1
                    | Abs(_, _, Const (\<^const_name>\<open>undefined\<close>, _)) => fst #> rev #> make_set T1
                    | _ => raise TERM ("post_process_term", [t]))
               | Type (\<^type_name>\<open>option\<close>, _) =>

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -96,7 +96,7 @@
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
     val eqs0 = [subst_v \<^term>\<open>0::natural\<close> eq,
-      subst_v (\<^const>\<open>Code_Numeral.Suc\<close> $ t_k) eq];
+      subst_v \<^Const>\<open>Code_Numeral.Suc for t_k\<close> eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, (_, eqs2)), lthy') = lthy
       |> BNF_LFP_Compat.primrec_simple

--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -550,8 +550,8 @@
           Symtab.join (K or3) (tab1, tab2)
         end
     val tab = go [] p (t, u) Symtab.empty
-    fun f (a, (true, false, false)) = SOME (a, \<^const>\<open>implies\<close>)
-      | f (a, (false, true, false)) = SOME (a, \<^const>\<open>rev_implies\<close>)
+    fun f (a, (true, false, false)) = SOME (a, \<^Const>\<open>implies\<close>)
+      | f (a, (false, true, false)) = SOME (a, \<^Const>\<open>rev_implies\<close>)
       | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)
       | f _                         = NONE
   in

--- a/src/HOL/Tools/record.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/record.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -1808,8 +1808,8 @@
      distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
      split_sels = [], split_sel_asms = [], case_eq_ifs = []};
 
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
-  | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+  | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
 
 fun add_spec_rule rule =
   let val head = head_of (lhs_of_equation (Thm.prop_of rule))

--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -250,8 +250,8 @@
     (map Pattern pats, Un (fm1', fm2'))
   end;
 
-fun mk_formula vs (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
-  | mk_formula vs (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
+fun mk_formula vs \<^Const_>\<open>conj for t1 t2\<close> = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
+  | mk_formula vs \<^Const_>\<open>disj for t1 t2\<close> = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
   | mk_formula vs t = apfst single (mk_atom vs t)
 
 fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2)