# HG changeset patch
# User wenzelm
# Date 1632861952 -7200
# Node ID bd9a5e128c31c33653d29554180ba1c28e9b7d84
# Parent  90c99974f6485ea3ffa0760b228f4fa8c35bab67# Parent  107941e8fa0140ac95aebeb3c6dc2a12802de30e
merged

diff -r 90c99974f648 -r bd9a5e128c31 NEWS
--- a/NEWS	Tue Sep 28 20:58:04 2021 +0200
+++ b/NEWS	Tue Sep 28 22:45:52 2021 +0200
@@ -279,12 +279,20 @@
 
     \<^Type>\<open>c\<close>
     \<^Type>\<open>c T \<dots>\<close>       \<comment> \<open>same with type arguments\<close>
-    \<^Type>_fn\<open>c T \<dots>\<close>    \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
+    \<^Type_fn>\<open>c T \<dots>\<close>    \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
     \<^Const>\<open>c\<close>
     \<^Const>\<open>c T \<dots>\<close>      \<comment> \<open>same with type arguments\<close>
     \<^Const>\<open>c for t \<dots>\<close>  \<comment> \<open>same with term arguments\<close>
     \<^Const_>\<open>c \<dots>\<close>       \<comment> \<open>same for patterns: case, let, fn\<close>
-    \<^Const>_fn\<open>c T \<dots>\<close>   \<comment> \<open>fn abstraction, failure via exception TERM\<close>
+    \<^Const_fn>\<open>c T \<dots>\<close>   \<comment> \<open>fn abstraction, failure via exception TERM\<close>
+
+The type/term arguments refer to nested ML source, which may contain
+antiquotations recursively. The following argument syntax is supported:
+
+  - an underscore (dummy pattern)
+  - an atomic item of "embedded" syntax, e.g. identifier or cartouche
+  - an antiquotation in control-symbol/cartouche form, e.g. \<^Type>\<open>c\<close>
+    as short form of \<open>\<^Type>\<open>c\<close>\<close>.
 
 Examples in HOL:
 
diff -r 90c99974f648 -r bd9a5e128c31 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/CCL/Wfd.thy	Tue Sep 28 22:45:52 2021 +0200
@@ -441,7 +441,7 @@
 
 fun is_rigid_prog t =
   (case (Logic.strip_assums_concl t) of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
   | _ => false)
 
 in
diff -r 90c99974f648 -r bd9a5e128c31 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/FOLP/IFOLP.thy	Tue Sep 28 22:45:52 2021 +0200
@@ -612,7 +612,7 @@
 structure Hypsubst = Hypsubst
 (
   (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq \<^Const_>\<open>Proof for \<open>\<^Const_>\<open>eq _ for t u\<close>\<close> _\<close> = (t, u);
+  fun dest_eq \<^Const_>\<open>Proof for \<^Const_>\<open>eq _ for t u\<close> _\<close> = (t, u);
 
   val imp_intr = @{thm impI}
 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 28 22:45:52 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)}]
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -58,7 +58,7 @@
   let
     val T = Term.range_type (Term.fastype_of t)
     val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
-  in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
+  in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end
 
 
 (*** Continuous function space ***)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -49,7 +49,7 @@
             Abs (_, T, _) => T
           | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
       in
-        \<^Const>\<open>case_prod T T2 \<open>\<^Type>\<open>bool\<close>\<close> for \<open>absfree (x, T) z\<close>\<close>
+        \<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close>
       end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy	Tue Sep 28 22:45:52 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 =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Tue Sep 28 22:45:52 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
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Library/code_test.ML	Tue Sep 28 22:45:52 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 =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -773,17 +773,17 @@
 
 fun is_first_order_lambda_free t =
   (case t of
-    \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
-  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
-  | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
-  | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
-  | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
-  | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
-    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
-  | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
-    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+    \<^Const_>\<open>Not for t1\<close> => is_first_order_lambda_free t1
+  | \<^Const_>\<open>All _ for \<open>Abs (_, _, t')\<close>\<close> => is_first_order_lambda_free t'
+  | \<^Const_>\<open>All _ for t1\<close> => is_first_order_lambda_free t1
+  | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, t')\<close>\<close> => is_first_order_lambda_free t'
+  | \<^Const_>\<open>Ex _ for t1\<close> => is_first_order_lambda_free t1
+  | \<^Const_>\<open>conj for t1 t2\<close> => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^Const_>\<open>disj for t1 t2\<close> => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^Const_>\<open>implies for t1 t2\<close> =>
+      is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =>
+      is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
 
 fun simple_translate_lambdas eta_matters do_lambdas ctxt type_enc t =
@@ -793,22 +793,22 @@
     let
       fun trans_first_order Ts t =
         (case t of
-          \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
-        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+          \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>trans_first_order Ts t1\<close>\<close>
+        | (t0 as \<^Const_>\<open>All _\<close>) $ Abs (s, T, t') =>
           t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+        | (t0 as \<^Const_>\<open>All _\<close>) $ t1 =>
           trans_first_order Ts (t0 $ eta_expand Ts t1 1)
-        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+        | (t0 as \<^Const_>\<open>Ex _\<close>) $ Abs (s, T, t') =>
           t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+        | (t0 as \<^Const_>\<open>Ex _\<close>) $ t1 =>
           trans_first_order Ts (t0 $ eta_expand Ts t1 1)
-        | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+        | (t0 as \<^Const_>\<open>conj\<close>) $ t1 $ t2 =>
           t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
-        | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+        | (t0 as \<^Const_>\<open>disj\<close>) $ t1 $ t2 =>
           t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
-        | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+        | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
           t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
-        | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
+        | (t0 as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 =>
           t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
         | _ =>
           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
@@ -1381,18 +1381,18 @@
       do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
     and do_formula bs pos t =
       (case t of
-        \<^const>\<open>Trueprop\<close> $ t1 => do_formula bs pos t1
-      | \<^const>\<open>Not\<close> $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
-      | Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t') => do_quant bs AForall pos s T t'
-      | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+        \<^Const_>\<open>Trueprop for t1\<close> => do_formula bs pos t1
+      | \<^Const_>\<open>Not for t1\<close> => do_formula bs (Option.map not pos) t1 #>> mk_anot
+      | \<^Const_>\<open>All _ for \<open>Abs (s, T, t')\<close>\<close> => do_quant bs AForall pos s T t'
+      | (t0 as \<^Const_>\<open>All _\<close>) $ t1 =>
         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
-      | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (s, T, t') => do_quant bs AExists pos s T t'
-      | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+      | \<^Const_>\<open>Ex _ for \<open>Abs (s, T, t')\<close>\<close> => do_quant bs AExists pos s T t'
+      | (t0 as \<^Const_>\<open>Ex _\<close>) $ t1 =>
         do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
-      | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
-      | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
-      | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => do_conn bs AImplies (Option.map not pos) t1 pos t2
-      | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
+      | \<^Const_>\<open>conj for t1 t2\<close> => do_conn bs AAnd pos t1 pos t2
+      | \<^Const_>\<open>disj for t1 t2\<close> => do_conn bs AOr pos t1 pos t2
+      | \<^Const_>\<open>implies for t1 t2\<close> => do_conn bs AImplies (Option.map not pos) t1 pos t2
+      | \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =>
         if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
       | _ => do_term bs t)
   in do_formula [] end
@@ -1449,7 +1449,7 @@
       |> presimplify_term simp_options ctxt
       |> HOLogic.dest_Trueprop
   end
-  handle TERM _ => \<^const>\<open>True\<close>
+  handle TERM _ => \<^Const>\<open>True\<close>
 
 (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
    reasons. *)
@@ -2030,9 +2030,9 @@
         end
   in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
 
-fun s_not_prop (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ s_not t
-  | s_not_prop (\<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>) = t
-  | s_not_prop t = \<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>
+fun s_not_prop \<^Const_>\<open>Trueprop for t\<close> = \<^Const>\<open>Trueprop for \<open>s_not t\<close>\<close>
+  | s_not_prop \<^Const_>\<open>Pure.imp for t \<^prop>\<open>False\<close>\<close> = t
+  | s_not_prop t = \<^Const>\<open>Pure.imp for t \<^prop>\<open>False\<close>\<close>
 
 fun translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t
       facts =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -127,7 +127,7 @@
     | (u, Const (\<^const_name>\<open>True\<close>, _)) => u
     | (Const (\<^const_name>\<open>False\<close>, _), v) => s_not v
     | (u, Const (\<^const_name>\<open>False\<close>, _)) => s_not u
-    | _ => if u aconv v then \<^const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
+    | _ => if u aconv v then \<^Const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
   | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
   | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
   | simplify_bool t = t
@@ -351,7 +351,7 @@
           error "Isar proof reconstruction failed because the ATP proof contains unparsable \
             \material"
         else if String.isPrefix native_type_prefix s then
-          \<^const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
+          \<^Const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
         else if s = tptp_equal then
           list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
             map (do_term [] NONE) us)
@@ -372,7 +372,7 @@
                     (nth us (length us - 2))
                 end
               else if s' = type_guard_name then
-                \<^const>\<open>True\<close> (* ignore type predicates *)
+                \<^Const>\<open>True\<close> (* ignore type predicates *)
               else
                 let
                   val new_skolem = String.isPrefix new_skolem_const_prefix s''
@@ -436,7 +436,7 @@
 fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
   if String.isPrefix class_prefix s then
     add_type_constraint pos (type_constraint_of_term ctxt u)
-    #> pair \<^const>\<open>True\<close>
+    #> pair \<^Const>\<open>True\<close>
   else
     pair (term_of_atp ctxt format type_enc textual sym_tab (SOME \<^typ>\<open>bool\<close>) u)
 
@@ -617,8 +617,8 @@
 
 fun repair_waldmeister_endgame proof =
   let
-    fun repair_tail (name, _, \<^const>\<open>Trueprop\<close> $ t, rule, deps) =
-      (name, Negated_Conjecture, \<^const>\<open>Trueprop\<close> $ s_not t, rule, deps)
+    fun repair_tail (name, _, \<^Const>\<open>Trueprop for t\<close>, rule, deps) =
+      (name, Negated_Conjecture, \<^Const>\<open>Trueprop for \<open>s_not t\<close>\<close>, rule, deps)
     fun repair_body [] = []
       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -261,43 +261,39 @@
 
 (* Simple simplifications to ensure that sort annotations don't leave a trail of
    spurious "True"s. *)
-fun s_not (Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', t')) =
-    Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', s_not t')
-  | s_not (Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', t')) =
-    Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', s_not t')
-  | s_not (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = \<^const>\<open>HOL.conj\<close> $ t1 $ s_not t2
-  | s_not (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
-    \<^const>\<open>HOL.disj\<close> $ s_not t1 $ s_not t2
-  | s_not (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
-    \<^const>\<open>HOL.conj\<close> $ s_not t1 $ s_not t2
-  | s_not (\<^const>\<open>False\<close>) = \<^const>\<open>True\<close>
-  | s_not (\<^const>\<open>True\<close>) = \<^const>\<open>False\<close>
-  | s_not (\<^const>\<open>Not\<close> $ t) = t
-  | s_not t = \<^const>\<open>Not\<close> $ t
+fun s_not \<^Const_>\<open>All T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>Ex T for \<open>Abs (s, T', s_not t')\<close>\<close>
+  | s_not \<^Const_>\<open>Ex T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>All T for \<open>Abs (s, T', s_not t')\<close>\<close>
+  | s_not \<^Const_>\<open>implies for t1 t2\<close> = \<^Const>\<open>conj for t1 \<open>s_not t2\<close>\<close>
+  | s_not \<^Const_>\<open>conj for t1 t2\<close> = \<^Const>\<open>disj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close> 
+  | s_not \<^Const_>\<open>disj for t1 t2\<close> = \<^Const>\<open>conj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close>
+  | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+  | s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+  | s_not \<^Const_>\<open>Not for t\<close> = t
+  | s_not t = \<^Const>\<open>Not for t\<close>
 
-fun s_conj (\<^const>\<open>True\<close>, t2) = t2
-  | s_conj (t1, \<^const>\<open>True\<close>) = t1
-  | s_conj (\<^const>\<open>False\<close>, _) = \<^const>\<open>False\<close>
-  | s_conj (_, \<^const>\<open>False\<close>) = \<^const>\<open>False\<close>
+fun s_conj (\<^Const_>\<open>True\<close>, t2) = t2
+  | s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+  | s_conj (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>False\<close>
+  | s_conj (_, \<^Const_>\<open>False\<close>) = \<^Const>\<open>False\<close>
   | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
 
-fun s_disj (\<^const>\<open>False\<close>, t2) = t2
-  | s_disj (t1, \<^const>\<open>False\<close>) = t1
-  | s_disj (\<^const>\<open>True\<close>, _) = \<^const>\<open>True\<close>
-  | s_disj (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close>
+fun s_disj (\<^Const_>\<open>False\<close>, t2) = t2
+  | s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+  | s_disj (\<^Const_>\<open>True\<close>, _) = \<^Const>\<open>True\<close>
+  | s_disj (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close>
   | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
 
-fun s_imp (\<^const>\<open>True\<close>, t2) = t2
-  | s_imp (t1, \<^const>\<open>False\<close>) = s_not t1
-  | s_imp (\<^const>\<open>False\<close>, _) = \<^const>\<open>True\<close>
-  | s_imp (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close>
+fun s_imp (\<^Const_>\<open>True\<close>, t2) = t2
+  | s_imp (t1, \<^Const_>\<open>False\<close>) = s_not t1
+  | s_imp (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>True\<close>
+  | s_imp (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close>
   | s_imp p = HOLogic.mk_imp p
 
-fun s_iff (\<^const>\<open>True\<close>, t2) = t2
-  | s_iff (t1, \<^const>\<open>True\<close>) = t1
-  | s_iff (\<^const>\<open>False\<close>, t2) = s_not t2
-  | s_iff (t1, \<^const>\<open>False\<close>) = s_not t1
-  | s_iff (t1, t2) = if t1 aconv t2 then \<^const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+fun s_iff (\<^Const_>\<open>True\<close>, t2) = t2
+  | s_iff (t1, \<^Const_>\<open>True\<close>) = t1
+  | s_iff (\<^Const_>\<open>False\<close>, t2) = s_not t2
+  | s_iff (t1, \<^Const_>\<open>False\<close>) = s_not t1
+  | s_iff (t1, t2) = if t1 aconv t2 then \<^Const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
@@ -352,18 +348,15 @@
     t
 
 fun unextensionalize_def t =
-  case t of
-    \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) =>
-    (case strip_comb lhs of
-       (c as Const (_, T), args) =>
-       if forall is_Var args andalso not (has_duplicates (op =) args) then
-         \<^const>\<open>Trueprop\<close>
-         $ (Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> \<^typ>\<open>bool\<close>)
-            $ c $ fold_rev lambda args rhs)
-       else
-         t
-     | _ => t)
-  | _ => t
+  (case t of
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> =>
+      (case strip_comb lhs of
+        (c as Const (_, T), args) =>
+          if forall is_Var args andalso not (has_duplicates (op =) args) then
+            \<^Const>\<open>Trueprop for \<^Const>\<open>HOL.eq T for c \<open>fold_rev lambda args rhs\<close>\<close>\<close>
+          else t
+      | _ => t)
+  | _ => t)
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
@@ -371,9 +364,8 @@
    "Meson_Clausify".) *)
 fun transform_elim_prop t =
   case Logic.strip_imp_concl t of
-    \<^const>\<open>Trueprop\<close> $ Var (z, \<^typ>\<open>bool\<close>) =>
-    subst_Vars [(z, \<^const>\<open>False\<close>)] t
-  | Var (z, \<^typ>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t
+    \<^Const_>\<open>Trueprop for \<open>Var (z, \<^typ>\<open>bool\<close>)\<close>\<close> => subst_Vars [(z, \<^Const>\<open>False\<close>)] t
+  | Var (z, \<^Type>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t
   | _ => t
 
 fun specialize_type thy (s, T) t =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Argo/argo_real.ML
--- a/src/HOL/Tools/Argo/argo_real.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -12,25 +12,25 @@
 fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
   | trans_type _ _ _ = NONE
 
-fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+fun trans_term f \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_neg |> SOME
-  | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
-  | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
-  | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
-  | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
-  | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>min \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
-  | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>max \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
-  | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+  | trans_term f \<^Const_>\<open>abs \<^Type>\<open>real\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_abs |> SOME
-  | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
-  | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+  | trans_term f \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
   | trans_term _ t tcx =
       (case try HOLogic.dest_number t of
@@ -40,12 +40,12 @@
 
 (* reverse translation *)
 
-fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close>
 fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_times t1 t2 = \<^Const>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close>
 
 fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
 
@@ -54,17 +54,17 @@
   in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
 
 fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
-  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
   | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
-      SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+      SOME \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
-      SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+      SOME \<^Const>\<open>min \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
-      SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
-  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+      SOME \<^Const>\<open>max \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
   | term_of _ _ = NONE
@@ -97,10 +97,10 @@
 
 local
 
-fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
+fun is_add2 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> = true
   | is_add2 _ = false
 
-fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ t\<close> = is_add2 t
   | is_add3 _ = false
 
 val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -600,7 +600,7 @@
 
 fun unclausify (thm, lits) ls =
   (case (Thm.prop_of thm, lits) of
-    (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
+    (\<^Const_>\<open>Trueprop for \<^Const_>\<open>False\<close>\<close>, [(_, ct)]) =>
       let val thm = Thm.implies_intr ct thm
       in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
   | _ => (thm, Ord_List.union lit_ord lits ls))
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -2215,7 +2215,7 @@
       let
         fun mk_goal c cps gcorec n k disc =
           mk_Trueprop_eq (disc $ (gcorec $ c),
-            if n = 1 then \<^const>\<open>True\<close>
+            if n = 1 then \<^Const>\<open>True\<close>
             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
         val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -42,7 +42,7 @@
   let
     fun instantiate_with_lambda thm =
       let
-        val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
+        val prop as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>HOL.eq _ for \<open>Var (_, fT) $ _\<close> _\<close>\<close>\<close> =
           Thm.prop_of thm;
         val T = range_type fT;
         val j = Term.maxidx_of_term prop + 1;
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -385,7 +385,7 @@
     val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
     val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
 
-    val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal;
+    val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> = code_goal;
     val (fun_t, args) = strip_comb lhs;
     val closed_rhs = fold_rev lambda args rhs;
 
@@ -447,7 +447,7 @@
 
     val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
 
-    fun is_nullary_disc_def (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
+    fun is_nullary_disc_def (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
           $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true
       | is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _
           $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
@@ -512,7 +512,7 @@
     val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho);
 
     fun const_of_transfer thm =
-      (case Thm.prop_of thm of \<^const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
+      (case Thm.prop_of thm of \<^Const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
 
     val eq_algrho =
       Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
@@ -590,7 +590,7 @@
 
 fun derive_cong_ctr_intros ctxt cong_ctor_intro =
   let
-    val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
+    val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
       Thm.prop_of cong_ctor_intro;
 
     val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor);
@@ -615,19 +615,19 @@
 
 fun derive_cong_friend_intro ctxt cong_algrho_intro =
   let
-    val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
+    val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
         $ ((algrho as Const (algrho_name, _)) $ _))) =
       Thm.prop_of cong_algrho_intro;
 
     val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
 
-    fun has_algrho (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
+    fun has_algrho (\<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
       fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
 
     val eq_algrho :: _ =
       maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
 
-    val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
+    val \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
     val friend = mk_ctr fp_argTs friend0;
 
     val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
@@ -654,8 +654,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val \<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
-        Abs (_, _, \<^const>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
+    val \<^Const_>\<open>Pure.imp\<close> $ (\<^Const_>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
+        Abs (_, _, \<^Const_>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
       Thm.prop_of dtor_coinduct;
 
     val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
@@ -820,7 +820,7 @@
             |> curry (op ~~) (map (fn disc => disc $ lhs) discs);
 
           fun mk_disc_iff_props props [] = props
-            | mk_disc_iff_props _ ((lhs, \<^const>\<open>HOL.True\<close>) :: _) = [lhs]
+            | mk_disc_iff_props _ ((lhs, \<^Const_>\<open>True\<close>) :: _) = [lhs]
             | mk_disc_iff_props props ((lhs, rhs) :: views) =
               mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views;
         in
@@ -2242,7 +2242,7 @@
 
     val fun_T =
       (case code_goal of
-        \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
+        \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
       | _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
     val fun_t = Const (fun_name, fun_T);
 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -367,7 +367,7 @@
           ctrXs_Tss
           |> map_index (fn (i, Ts) =>
             Abs (Name.uu, mk_tupleT_balanced Ts,
-              if i + 1 = k then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>))
+              if i + 1 = k then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>))
           |> mk_case_sumN_balanced
           |> map_types substXYT
           |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -189,22 +189,22 @@
 
 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
-val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>;
-val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>;
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^Const>\<open>True\<close>;
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^Const>\<open>False\<close>;
 val mk_dnf = mk_disjs o map mk_conjs;
 
-val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts;
+val conjuncts_s = filter_out (curry (op aconv) \<^Const>\<open>True\<close>) o HOLogic.conjuncts;
 
-fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
-  | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
-  | s_not (\<^const>\<open>Not\<close> $ t) = t
-  | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u
-  | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u
-  | s_not t = \<^const>\<open>Not\<close> $ t;
+fun s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+  | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+  | s_not \<^Const_>\<open>Not for t\<close> = t
+  | s_not \<^Const_>\<open>conj for t u\<close> = \<^Const>\<open>disj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+  | s_not \<^Const_>\<open>disj for t u\<close> = \<^Const>\<open>conj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+  | s_not t = \<^Const>\<open>Not for t\<close>;
 
 val s_not_conj = conjuncts_s o s_not o mk_conjs;
 
-fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs;
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^Const>\<open>False\<close>] else cs;
 fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
 
 fun propagate_units css =
@@ -215,17 +215,17 @@
       (map (propagate_unit_pos u) (uss @ css'))));
 
 fun s_conjs cs =
-  if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
-  else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs);
+  if member (op aconv) cs \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
+  else mk_conjs (remove (op aconv) \<^Const>\<open>True\<close> cs);
 
 fun s_disjs ds =
-  if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
-  else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds);
+  if member (op aconv) ds \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
+  else mk_disjs (remove (op aconv) \<^Const>\<open>False\<close> ds);
 
 fun s_dnf css0 =
   let val css = propagate_units css0 in
     if null css then
-      [\<^const>\<open>False\<close>]
+      [\<^Const>\<open>False\<close>]
     else if exists null css then
       []
     else
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -154,7 +154,7 @@
 
 fun inst_split_eq ctxt split =
   (case Thm.prop_of split of
-    \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var (_, Type (_, [T, _])) $ _\<close> _\<close>\<close> =>
     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/BNF/bnf_lfp_countable.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -70,13 +70,13 @@
 
 fun encode_sumN n k t =
   Balanced_Tree.access {init = t,
-      left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
-      right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
+      left = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inl \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>,
+      right = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inr \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>}
     n k;
 
-fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
+fun encode_tuple [] = \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>
   | encode_tuple ts =
-    Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+    Balanced_Tree.make (fn (t, u) => \<^Const>\<open>prod_encode for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for u t\<close>\<close>) ts;
 
 fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
   let
@@ -181,7 +181,7 @@
       |> map (Thm.close_derivation \<^here>)
     end;
 
-fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
     $ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
         $ Const (\<^const_name>\<open>top\<close>, _)))) = s
   | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 28 22:45:52 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) =>
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Sep 28 22:45:52 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;
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -261,9 +261,9 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (Thm.concl_of th) of
-          \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
+          \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close> =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
+        | \<^Const_>\<open>disj for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t u\<close>\<close> _\<close> =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
@@ -271,7 +271,7 @@
         | _ => (*not a disjunction*) th;
 
 fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q
-  | notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1
+  | notequal_lits_count \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for _ _\<close>\<close> = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -414,7 +414,7 @@
 
 (**** Generation of contrapositives ****)
 
-fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
+fun is_left \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close>\<close> = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -435,7 +435,7 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for t _\<close>\<close> = rigid t
   | ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4horn _ = false;
 
@@ -470,7 +470,7 @@
 
 (***** MESON PROOF PROCEDURE *****)
 
-fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for A\<close> phi\<close>, As) = rhyps(phi, A::As)
   | rhyps (_, As) = As;
 
 (** Detecting repeated assumptions in a subgoal **)
@@ -514,7 +514,7 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for t\<close>\<close> = rigid t
   | ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4nnf _ = false;
 
@@ -620,7 +620,7 @@
 (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
 fun cong_extensionalize_thm ctxt th =
   (case Thm.concl_of th of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> =>
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close> =>
       (case get_F_pattern T t u of
         SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
       | NONE => th)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -182,8 +182,7 @@
 
 fun none_true assigns = forall (not_equal (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 =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -331,16 +331,16 @@
   else
     s
 
-fun s_conj (t1, \<^const>\<open>True\<close>) = t1
-  | s_conj (\<^const>\<open>True\<close>, t2) = t2
+fun s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+  | s_conj (\<^Const_>\<open>True\<close>, t2) = t2
   | s_conj (t1, t2) =
-    if t1 = \<^const>\<open>False\<close> orelse t2 = \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
+    if t1 = \<^Const>\<open>False\<close> orelse t2 = \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
     else HOLogic.mk_conj (t1, t2)
 
-fun s_disj (t1, \<^const>\<open>False\<close>) = t1
-  | s_disj (\<^const>\<open>False\<close>, t2) = t2
+fun s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+  | s_disj (\<^Const_>\<open>False\<close>, t2) = t2
   | s_disj (t1, t2) =
-    if t1 = \<^const>\<open>True\<close> orelse t2 = \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
+    if t1 = \<^Const>\<open>True\<close> orelse t2 = \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
     else HOLogic.mk_disj (t1, t2)
 
 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -348,13 +348,13 @@
   | strip_connective _ t = [t]
 
 fun strip_any_connective (t as (t0 $ _ $ _)) =
-    if t0 = \<^const>\<open>HOL.conj\<close> orelse t0 = \<^const>\<open>HOL.disj\<close> then
+    if t0 = \<^Const>\<open>conj\<close> orelse t0 = \<^Const>\<open>disj\<close> then
       (strip_connective t0 t, t0)
     else
-      ([t], \<^const>\<open>Not\<close>)
-  | strip_any_connective t = ([t], \<^const>\<open>Not\<close>)
-val conjuncts_of = strip_connective \<^const>\<open>HOL.conj\<close>
-val disjuncts_of = strip_connective \<^const>\<open>HOL.disj\<close>
+      ([t], \<^Const>\<open>Not\<close>)
+  | strip_any_connective t = ([t], \<^Const>\<open>Not\<close>)
+val conjuncts_of = strip_connective \<^Const>\<open>conj\<close>
+val disjuncts_of = strip_connective \<^Const>\<open>disj\<close>
 
 (* When you add constants to these lists, make sure to handle them in
    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -797,8 +797,8 @@
         the (Quotient_Info.lookup_quotients thy s)
       val partial =
         case Thm.prop_of equiv_thm of
-          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
-        | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
+          \<^Const_>\<open>Trueprop for \<^Const_>\<open>equivp _ for _\<close>\<close> => false
+        | \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
         | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
                                    \relation theorem"
       val Ts' = qtyp |> dest_Type |> snd
@@ -948,7 +948,7 @@
       fold (fn (z as ((s, _), T)) => fn t' =>
                Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
            (take (length zs' - length zs) zs')
-    fun aux zs (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
+    fun aux zs \<^Const>\<open>Pure.imp for t1 t2\<close> =
         let val zs' = Term.add_vars t1 zs in
           close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
         end
@@ -957,8 +957,8 @@
 
 fun distinctness_formula T =
   all_distinct_unordered_pairs_of
-  #> map (fn (t1, t2) => \<^const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
-  #> List.foldr (s_conj o swap) \<^const>\<open>True\<close>
+  #> map (fn (t1, t2) => \<^Const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
+  #> List.foldr (s_conj o swap) \<^Const>\<open>True\<close>
 
 fun zero_const T = Const (\<^const_name>\<open>zero_class.zero\<close>, T)
 fun suc_const T = Const (\<^const_name>\<open>Suc\<close>, T --> T)
@@ -986,7 +986,7 @@
                SOME {abs_type, rep_type, Abs_name, ...} =>
                [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
              | NONE =>
-               if T = \<^typ>\<open>ind\<close> then [dest_Const \<^const>\<open>Zero_Rep\<close>, dest_Const \<^const>\<open>Suc_Rep\<close>]
+               if T = \<^typ>\<open>ind\<close> then [dest_Const \<^Const>\<open>Zero_Rep\<close>, dest_Const \<^Const>\<open>Suc_Rep\<close>]
                else [])
   | uncached_data_type_constrs _ _ = []
 
@@ -1145,8 +1145,8 @@
     if t1' aconv t2 then \<^prop>\<open>True\<close> else t1 $ t2
   | s_betapply _ (t1 as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1', t2) =
     if t1' aconv t2 then \<^term>\<open>True\<close> else t1 $ t2
-  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>True\<close> $ t1', _) = t1'
-  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>False\<close> $ _, t2) = t2
+  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>True\<close> $ t1', _) = t1'
+  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>False\<close> $ _, t2) = t2
   | s_betapply Ts (Const (\<^const_name>\<open>Let\<close>,
                           Type (_, [bound_T, Type (_, [_, body_T])]))
                    $ t12 $ Abs (s, T, t13'), t2) =
@@ -1181,18 +1181,18 @@
 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   let val dataT = body_type T in
     if s = \<^const_name>\<open>Suc\<close> then
-      Abs (Name.uu, dataT, \<^const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
+      Abs (Name.uu, dataT, \<^Const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
     else if length (data_type_constrs hol_ctxt dataT) >= 2 then
       Const (discr_for_constr x)
     else
-      Abs (Name.uu, dataT, \<^const>\<open>True\<close>)
+      Abs (Name.uu, dataT, \<^Const>\<open>True\<close>)
   end
 
 fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
   case head_of t of
     Const x' =>
-    if x = x' then \<^const>\<open>True\<close>
-    else if is_nonfree_constr ctxt x' then \<^const>\<open>False\<close>
+    if x = x' then \<^Const>\<open>True\<close>
+    else if is_nonfree_constr ctxt x' then \<^Const>\<open>False\<close>
     else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
 
@@ -1379,10 +1379,10 @@
    simplification rules (equational specifications). *)
 fun term_under_def t =
   case t of
-    \<^const>\<open>Pure.imp\<close> $ _ $ t2 => term_under_def t2
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => term_under_def t1
-  | \<^const>\<open>Trueprop\<close> $ t1 => term_under_def t1
-  | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => term_under_def t1
+    \<^Const_>\<open>Pure.imp for _ t2\<close> => term_under_def t2
+  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => term_under_def t1
+  | \<^Const_>\<open>Trueprop for t1\<close> => term_under_def t1
+  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => term_under_def t1
   | Abs (_, _, t') => term_under_def t'
   | t1 $ _ => term_under_def t1
   | _ => t
@@ -1405,9 +1405,8 @@
       | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
-        Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => (t1, t2)
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
-        (t1, t2)
+        \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => (t1, t2)
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close> => (t1, t2)
       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
     val args = strip_comb lhs |> snd
   in fold_rev aux args (SOME rhs) end
@@ -1482,13 +1481,13 @@
 
 fun lhs_of_equation t =
   case t of
-    Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => SOME t1
-  | \<^const>\<open>Pure.imp\<close> $ _ $ t2 => lhs_of_equation t2
-  | \<^const>\<open>Trueprop\<close> $ t1 => lhs_of_equation t1
-  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
-  | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => SOME t1
-  | \<^const>\<open>HOL.implies\<close> $ _ $ t2 => lhs_of_equation t2
+    \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => SOME t1
+  | \<^Const_>\<open>Pure.imp for _ t2\<close> => lhs_of_equation t2
+  | \<^Const_>\<open>Trueprop for t1\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>All _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => SOME t1
+  | \<^Const_>\<open>implies for _ t2\<close> => lhs_of_equation t2
   | _ => NONE
 
 fun is_constr_pattern _ (Bound _) = true
@@ -1598,19 +1597,19 @@
                                    (incr_boundvars 1 func_t, x),
                   discriminate_value hol_ctxt x (Bound 0)))
       |> AList.group (op aconv)
-      |> map (apsnd (List.foldl s_disj \<^const>\<open>False\<close>))
+      |> map (apsnd (List.foldl s_disj \<^Const>\<open>False\<close>))
       |> sort (int_ord o apply2 (size_of_term o snd))
       |> rev
   in
     if res_T = bool_T then
-      if forall (member (op =) [\<^const>\<open>False\<close>, \<^const>\<open>True\<close>] o fst) cases then
+      if forall (member (op =) [\<^Const>\<open>False\<close>, \<^Const>\<open>True\<close>] o fst) cases then
         case cases of
           [(body_t, _)] => body_t
-        | [_, (\<^const>\<open>True\<close>, head_t2)] => head_t2
-        | [_, (\<^const>\<open>False\<close>, head_t2)] => \<^const>\<open>Not\<close> $ head_t2
+        | [_, (\<^Const>\<open>True\<close>, head_t2)] => head_t2
+        | [_, (\<^Const>\<open>False\<close>, head_t2)] => \<^Const>\<open>Not for head_t2\<close>
         | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
       else
-        \<^const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
+        \<^Const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
     else
       fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
   end
@@ -1895,13 +1894,12 @@
   in
     Logic.list_implies (prems,
         case concl of
-          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
-                               $ t1 $ t2) =>
-          \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
-        | \<^const>\<open>Trueprop\<close> $ t' =>
-          \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (t', \<^const>\<open>True\<close>)
-        | Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
-          \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
+          \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for t1 t2\<close>\<close> =>
+          \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
+        | \<^Const_>\<open>Trueprop for t'\<close> =>
+          \<^Const>\<open>Trueprop for \<open>HOLogic.mk_eq (t', \<^Const>\<open>True\<close>)\<close>\<close>
+        | \<^Const_>\<open>Pure.eq T for t1 t2\<close> =>
+          \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
         | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
                          quote (Syntax.string_of_term ctxt t));
                 raise SAME ()))
@@ -1951,7 +1949,7 @@
   end
 
 fun ground_theorem_table thy =
-  fold ((fn \<^const>\<open>Trueprop\<close> $ t1 =>
+  fold ((fn \<^Const_>\<open>Trueprop for t1\<close> =>
             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
           | _ => I) o Thm.prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
 
@@ -2016,13 +2014,13 @@
   in
     [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
      Logic.list_implies
-         ([\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
-           \<^const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
+         ([\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
+           \<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
            equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
            Logic.mk_equals (normal_x, normal_y)),
      Logic.list_implies
-         ([HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
-           HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
+         ([HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
+           HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
     |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
   end
@@ -2031,8 +2029,8 @@
   let
     val xs = data_type_constrs hol_ctxt T
     val pred_T = T --> bool_T
-    val iter_T = \<^typ>\<open>bisim_iterator\<close>
-    val bisim_max = \<^const>\<open>bisim_iterator_max\<close>
+    val iter_T = \<^Type>\<open>bisim_iterator\<close>
+    val bisim_max = \<^Const>\<open>bisim_iterator_max\<close>
     val n_var = Var (("n", 0), iter_T)
     val n_var_minus_1 =
       Const (\<^const_name>\<open>safe_The\<close>, (iter_T --> bool_T) --> iter_T)
@@ -2214,8 +2212,8 @@
           fun repair_rec j (Const (\<^const_name>\<open>Ex\<close>, T1) $ Abs (s2, T2, t2')) =
               Const (\<^const_name>\<open>Ex\<close>, T1)
               $ Abs (s2, T2, repair_rec (j + 1) t2')
-            | repair_rec j (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
-              \<^const>\<open>HOL.conj\<close> $ repair_rec j t1 $ repair_rec j t2
+            | repair_rec j \<^Const_>\<open>conj for t1 t2\<close> =
+              \<^Const>\<open>conj for \<open>repair_rec j t1\<close> \<open>repair_rec j t2\<close>\<close>
             | repair_rec j t =
               let val (head, args) = strip_comb t in
                 if head = Bound j then
@@ -2227,9 +2225,9 @@
           val (nonrecs, recs) =
             List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
                            (disjuncts_of body)
-          val base_body = nonrecs |> List.foldl s_disj \<^const>\<open>False\<close>
+          val base_body = nonrecs |> List.foldl s_disj \<^Const>\<open>False\<close>
           val step_body = recs |> map (repair_rec j)
-                               |> List.foldl s_disj \<^const>\<open>False\<close>
+                               |> List.foldl s_disj \<^Const>\<open>False\<close>
         in
           (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
            |> ap_n_split (length arg_Ts) tuple_T bool_T,
@@ -2241,11 +2239,7 @@
   in aux end
 
 fun predicatify T t =
-  let val set_T = HOLogic.mk_setT T in
-    Abs (Name.uu, T,
-         Const (\<^const_name>\<open>Set.member\<close>, T --> set_T --> bool_T)
-         $ Bound 0 $ incr_boundvars 1 t)
-  end
+  Abs (Name.uu, T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> \<open>incr_boundvars 1 t\<close>\<close>)
 
 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
   let
@@ -2365,7 +2359,7 @@
                       [inductive_pred_axiom hol_ctxt x]
                     else case def_of_const thy def_tables x of
                       SOME def =>
-                      \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
+                      \<^Const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
                       |> equationalize_term ctxt "" |> the |> single
                     | NONE => [])
            | psimps => psimps)
@@ -2373,7 +2367,7 @@
 
 fun is_equational_fun_surely_complete hol_ctxt x =
   case equational_fun_axioms hol_ctxt x of
-    [\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
+    [\<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 _\<close>\<close>] =>
     strip_comb t1 |> snd |> forall is_Var
   | _ => false
 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -333,8 +333,8 @@
         else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
   in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
 
-fun truth_const_sort_key \<^const>\<open>True\<close> = "0"
-  | truth_const_sort_key \<^const>\<open>False\<close> = "2"
+fun truth_const_sort_key \<^Const_>\<open>True\<close> = "0"
+  | truth_const_sort_key \<^Const_>\<open>False\<close> = "2"
   | truth_const_sort_key _ = "1"
 
 fun mk_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) ts =
@@ -411,14 +411,14 @@
               empty_const
           | aux ((t1, t2) :: zs) =
             aux zs
-            |> t2 <> \<^const>\<open>False\<close>
+            |> t2 <> \<^Const>\<open>False\<close>
                ? curry (op $)
                        (insert_const
-                        $ (t1 |> t2 <> \<^const>\<open>True\<close>
+                        $ (t1 |> t2 <> \<^Const>\<open>True\<close>
                                  ? curry (op $)
                                          (Const (maybe_name, T --> T))))
       in
-        if forall (fn (_, t) => t <> \<^const>\<open>True\<close> andalso t <> \<^const>\<open>False\<close>)
+        if forall (fn (_, t) => t <> \<^Const>\<open>True\<close> andalso t <> \<^Const>\<open>False\<close>)
                   tps then
           Const (unknown, set_T)
         else
@@ -516,7 +516,7 @@
       | term_for_atom seen \<^typ>\<open>prop\<close> _ j k =
         HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
       | term_for_atom _ \<^typ>\<open>bool\<close> _ j _ =
-        if j = 0 then \<^const>\<open>False\<close> else \<^const>\<open>True\<close>
+        if j = 0 then \<^Const>\<open>False\<close> else \<^Const>\<open>True\<close>
       | term_for_atom seen T _ j k =
         if T = nat_T then
           HOLogic.mk_number nat_T j
@@ -524,7 +524,7 @@
           HOLogic.mk_number int_T (int_for_atom (k, 0) j)
         else if is_fp_iterator_type T then
           HOLogic.mk_number nat_T (k - j - 1)
-        else if T = \<^typ>\<open>bisim_iterator\<close> then
+        else if T = \<^Type>\<open>bisim_iterator\<close> then
           HOLogic.mk_number nat_T j
         else case data_type_spec data_types T of
           NONE => nth_atom thy atomss pool T j
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -829,10 +829,10 @@
                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
                            " : _?");
        case t of
-         \<^const>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
+         \<^Const_>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
        | Const (\<^const_name>\<open>None\<close>, T) =>
          (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
-       | \<^const>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
+       | \<^Const_>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
        | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ Bound 0 $ t2 =>
          (* hack to exploit symmetry of equality when typing "insert" *)
          (if t2 = Bound 0 then do_term \<^term>\<open>True\<close>
@@ -850,9 +850,9 @@
             | \<^const_name>\<open>Ex\<close> =>
               let val set_T = domain_type T in
                 do_term (Abs (Name.uu, set_T,
-                              \<^const>\<open>Not\<close> $ (HOLogic.mk_eq
+                              \<^Const>\<open>Not\<close> $ (HOLogic.mk_eq
                                   (Abs (Name.uu, domain_type set_T,
-                                        \<^const>\<open>False\<close>),
+                                        \<^Const>\<open>False\<close>),
                                    Bound 0)))) accum
               end
             | \<^const_name>\<open>HOL.eq\<close> => do_equals T accum
@@ -971,12 +971,11 @@
                         val (M', accum) =
                           do_term t' (accum |>> push_bound (V x) T M)
                       in (MFun (M, V x, M'), accum |>> pop_bound) end))
-         | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec t1 \<^const>\<open>False\<close> accum
-         | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec t1 t2 accum
-         | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec t1 t2 accum
-         | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec t1 t2 accum
-         | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
-           do_term (betapply (t2, t1)) accum
+         | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec t1 \<^Const>\<open>False\<close> accum
+         | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec t1 t2 accum
+         | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec t1 t2 accum
+         | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec t1 t2 accum
+         | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_term (betapply (t2, t1)) accum
          | t1 $ t2 =>
            let
              fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
@@ -1060,7 +1059,7 @@
           Const (s as \<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) =>
           do_quantifier s T1 t1
         | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
-        | \<^const>\<open>Trueprop\<close> $ t1 => do_formula sn t1 accum
+        | \<^Const_>\<open>Trueprop for t1\<close> => do_formula sn t1 accum
         | Const (s as \<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) =>
           do_quantifier s T1 t1
         | Const (s as \<^const_name>\<open>Ex\<close>, T0) $ (t1 as Abs (_, T1, t1')) =>
@@ -1068,19 +1067,17 @@
              Plus => do_quantifier s T1 t1'
            | Minus =>
              (* FIXME: Needed? *)
-             do_term (\<^const>\<open>Not\<close>
+             do_term (\<^Const>\<open>Not\<close>
                       $ (HOLogic.eq_const (domain_type T0) $ t1
-                         $ Abs (Name.uu, T1, \<^const>\<open>False\<close>))) accum)
-        | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
-        | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
-          do_formula sn (betapply (t2, t1)) accum
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          do_connect meta_conj_spec false t1 t2 accum
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
-        | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec true t1 \<^const>\<open>False\<close> accum
-        | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
-        | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
-        | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
+                         $ Abs (Name.uu, T1, \<^Const>\<open>False\<close>))) accum)
+        | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => do_equals t1 t2
+        | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_formula sn (betapply (t2, t1)) accum
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => do_connect meta_conj_spec false t1 t2 accum
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_connect meta_imp_spec true t1 t2 accum
+        | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec true t1 \<^Const>\<open>False\<close> accum
+        | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec false t1 t2 accum
+        | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec false t1 t2 accum
+        | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec true t1 t2 accum
         | _ => do_term t accum
       end
       |> tap (fn (gamma, _) =>
@@ -1122,18 +1119,15 @@
       and do_implies t1 t2 = do_term t1 #> do_formula t2
       and do_formula t accum =
         case t of
-          Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
-        | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1 accum
-        | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 =>
-          consider_general_equals mdata true t1 t2 accum
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_implies t1 t2 accum
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          fold (do_formula) [t1, t2] accum
-        | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
-        | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 =>
-          consider_general_equals mdata true t1 t2 accum
-        | \<^const>\<open>conj\<close> $ t1 $ t2 => fold (do_formula) [t1, t2] accum
-        | \<^const>\<open>implies\<close> $ t1 $ t2 => do_implies t1 t2 accum
+          \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+        | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1 accum
+        | \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_implies t1 t2 accum
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+        | \<^Const_>\<open>All _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+        | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+        | \<^Const_>\<open>conj for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+        | \<^Const_>\<open>implies for t1 t2\<close> => do_implies t1 t2 accum
         | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                            \do_formula", [t])
     in do_formula t end
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -36,15 +36,12 @@
 
 val may_use_binary_ints =
   let
-    fun aux def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) =
-        aux def t1 andalso aux false t2
-      | aux def (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
-      | aux def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =
-        aux def t1 andalso aux false t2
-      | aux def (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
+    fun aux def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+      | aux def \<^Const_>\<open>Pure.imp for t1 t2\<close> = aux false t1 andalso aux def t2
+      | aux def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+      | aux def \<^Const_>\<open>implies for t1 t2\<close> = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
-      | aux def (t as Const (s, _)) =
-        (not def orelse t <> \<^const>\<open>Suc\<close>) andalso
+      | aux def (t as Const (s, _)) = (not def orelse t <> \<^Const>\<open>Suc\<close>) andalso
         not (member (op =)
                [\<^const_name>\<open>Abs_Frac\<close>, \<^const_name>\<open>Rep_Frac\<close>,
                 \<^const_name>\<open>nat_gcd\<close>, \<^const_name>\<open>nat_lcm\<close>,
@@ -143,7 +140,7 @@
       | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
       case t of
-        \<^const>\<open>Trueprop\<close> $ t1 => box_var_in_def new_Ts old_Ts t1 z
+        \<^Const_>\<open>Trueprop for t1\<close> => box_var_in_def new_Ts old_Ts t1 z
       | Const (s0, _) $ t1 $ _ =>
         if s0 = \<^const_name>\<open>Pure.eq\<close> orelse s0 = \<^const_name>\<open>HOL.eq\<close> then
           let
@@ -190,31 +187,29 @@
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>Pure.eq\<close>, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
-        \<^const>\<open>Pure.imp\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-        \<^const>\<open>Pure.conjunction\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>Trueprop\<close> $ t1 =>
-        \<^const>\<open>Trueprop\<close> $ do_term new_Ts old_Ts polar t1
-      | \<^const>\<open>Not\<close> $ t1 =>
-        \<^const>\<open>Not\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
+      | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+        \<^Const>\<open>Pure.imp for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+        \<^Const>\<open>Pure.conjunction for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>Trueprop for t1\<close> => \<^Const>\<open>Trueprop for \<open>do_term new_Ts old_Ts polar t1\<close>\<close>
+      | \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>\<close>
       | Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>HOL.eq\<close>, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.conj\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.disj\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.implies\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
-        $ do_term new_Ts old_Ts polar t2
+      | \<^Const_>\<open>conj for t1 t2\<close> =>
+        \<^Const>\<open>conj for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>disj for t1 t2\<close> =>
+        \<^Const>\<open>disj for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>implies for t1 t2\<close> =>
+        \<^Const>\<open>implies for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
       | Const (x as (s, T)) =>
         if is_descr s then
           do_descr s T
@@ -335,11 +330,11 @@
       case t of
         (t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2 =>
+      | (t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2 =>
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
       | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+      | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -402,11 +397,11 @@
                     | _ => I) t (K 0)
     fun aux Ts careful ((t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2) =
         aux_eq Ts careful true t0 t1 t2
-      | aux Ts careful ((t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2) =
+      | aux Ts careful ((t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2) =
         t0 $ aux Ts false t1 $ aux Ts careful t2
       | aux Ts careful ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2) =
         aux_eq Ts careful true t0 t1 t2
-      | aux Ts careful ((t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2) =
+      | aux Ts careful ((t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2) =
         t0 $ aux Ts false t1 $ aux Ts careful t2
       | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
       | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
@@ -417,13 +412,13 @@
           raise SAME ()
         else if axiom andalso is_Var t2 andalso
                 num_occs_of_var (dest_Var t2) = 1 then
-          \<^const>\<open>True\<close>
+          \<^Const>\<open>True\<close>
         else case strip_comb t2 of
           (* The first case is not as general as it could be. *)
           (Const (\<^const_name>\<open>PairBox\<close>, _),
                   [Const (\<^const_name>\<open>fst\<close>, _) $ Var z1,
                    Const (\<^const_name>\<open>snd\<close>, _) $ Var z2]) =>
-          if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^const>\<open>True\<close>
+          if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^Const>\<open>True\<close>
           else raise SAME ()
         | (Const (x as (s, T)), args) =>
           let
@@ -454,26 +449,22 @@
 
 (** Destruction of universal and existential equalities **)
 
-fun curry_assms (\<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close>
-                                   $ (\<^const>\<open>HOL.conj\<close> $ t1 $ t2)) $ t3) =
+fun curry_assms \<^Const_>\<open>Pure.imp for \<^Const>\<open>Trueprop for \<^Const_>\<open>conj for t1 t2\<close>\<close> t3\<close> =
     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
-  | curry_assms (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
-    \<^const>\<open>Pure.imp\<close> $ curry_assms t1 $ curry_assms t2
+  | curry_assms \<^Const_>\<open>Pure.imp for t1 t2\<close> = \<^Const>\<open>Pure.imp for \<open>curry_assms t1\<close> \<open>curry_assms t2\<close>\<close>
   | curry_assms t = t
 
 val destroy_universal_equalities =
   let
     fun aux prems zs t =
       case t of
-        \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => aux_implies prems zs t1 t2
+        \<^Const_>\<open>Pure.imp for t1 t2\<close> => aux_implies prems zs t1 t2
       | _ => Logic.list_implies (rev prems, t)
     and aux_implies prems zs t1 t2 =
       case t1 of
-        Const (\<^const_name>\<open>Pure.eq\<close>, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var z $ t') =>
-        aux_eq prems zs z t' t1 t2
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ Var z) =>
-        aux_eq prems zs z t' t1 t2
+        \<^Const_>\<open>Pure.eq _ for \<open>Var z\<close> t'\<close> => aux_eq prems zs z t' t1 t2
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var z\<close> t'\<close>\<close> => aux_eq prems zs z t' t1 t2
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t' \<open>Var z\<close>\<close>\<close> => aux_eq prems zs z t' t1 t2
       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
     and aux_eq prems zs z t' t1 t2 =
       if not (member (op =) zs z) andalso
@@ -528,7 +519,7 @@
     fun kill [] [] ts = foldr1 s_conj ts
       | kill (s :: ss) (T :: Ts) ts =
         (case find_bound_assign ctxt (length ss) [] ts of
-           SOME (_, []) => \<^const>\<open>True\<close>
+           SOME (_, []) => \<^Const>\<open>True\<close>
          | SOME (arg_t, ts) =>
            kill ss Ts (map (subst_one_bound (length ss)
                                 (incr_bv (~1, length ss + 1, arg_t))) ts)
@@ -592,27 +583,27 @@
         case t of
           Const (s0 as \<^const_name>\<open>Pure.all\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
-          \<^const>\<open>Pure.imp\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
-          $ aux ss Ts js skolemizable polar t2
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          \<^const>\<open>Pure.conjunction\<close> $ aux ss Ts js skolemizable polar t1
-          $ aux ss Ts js skolemizable polar t2
-        | \<^const>\<open>Trueprop\<close> $ t1 =>
-          \<^const>\<open>Trueprop\<close> $ aux ss Ts js skolemizable polar t1
-        | \<^const>\<open>Not\<close> $ t1 =>
-          \<^const>\<open>Not\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+          \<^Const>\<open>Pure.imp for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+          \<^Const>\<open>Pure.conjunction for \<open>aux ss Ts js skolemizable polar t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+        | \<^Const_>\<open>Trueprop for t1\<close> =>
+          \<^Const>\<open>Trueprop for \<open>aux ss Ts js skolemizable polar t1\<close>\<close>
+        | \<^Const_>\<open>Not for t1\<close> =>
+          \<^Const>\<open>Not for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>\<close>
         | Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
         | Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
+        | \<^Const_>\<open>conj for t1 t2\<close> =>
           s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
-        | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
+        | \<^Const_>\<open>disj for t1 t2\<close> =>
           s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
-        | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
-          \<^const>\<open>HOL.implies\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
-          $ aux ss Ts js skolemizable polar t2
+        | \<^Const_>\<open>implies for t1 t2\<close> =>
+          \<^Const>\<open>implies for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
         | (t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js skolemizable polar t2
         | Const (x as (s, T)) =>
@@ -622,8 +613,8 @@
             let
               val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
               val (pref, connective) =
-                if gfp then (lbfp_prefix, \<^const>\<open>HOL.disj\<close>)
-                else (ubfp_prefix, \<^const>\<open>HOL.conj\<close>)
+                if gfp then (lbfp_prefix, \<^Const>\<open>disj\<close>)
+                else (ubfp_prefix, \<^Const>\<open>conj\<close>)
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
                            |> aux ss Ts js skolemizable polar
               fun neg () = Const (pref ^ s, T)
@@ -653,10 +644,9 @@
 
 (** Function specialization **)
 
-fun params_in_equation (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = params_in_equation t2
-  | params_in_equation (\<^const>\<open>Trueprop\<close> $ t1) = params_in_equation t1
-  | params_in_equation (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _) =
-    snd (strip_comb t1)
+fun params_in_equation \<^Const_>\<open>Pure.imp for _ t2\<close> = params_in_equation t2
+  | params_in_equation \<^Const_>\<open>Trueprop for t1\<close> = params_in_equation t1
+  | params_in_equation \<^Const_>\<open>HOL.eq _ for t1 _\<close> = snd (strip_comb t1)
   | params_in_equation _ = []
 
 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
@@ -865,10 +855,8 @@
       if exists_subterm (curry (op aconv) u) def then NONE else SOME u
   in
     case t of
-      Const (\<^const_name>\<open>Pure.eq\<close>, _) $ (u as Free _) $ def => do_equals u def
-    | \<^const>\<open>Trueprop\<close>
-      $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (u as Free _) $ def) =>
-      do_equals u def
+      \<^Const_>\<open>Pure.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
+    | \<^Const_>\<open>Trueprop\<close> $ \<^Const_>\<open>HOL.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
     | _ => NONE
   end
 
@@ -917,7 +905,7 @@
     and add_def_axiom depth = add_axiom fst apfst true depth
     and add_nondef_axiom depth = add_axiom snd apsnd false depth
     and add_maybe_def_axiom depth t =
-      (if head_of t <> \<^const>\<open>Pure.imp\<close> then add_def_axiom
+      (if head_of t <> \<^Const>\<open>Pure.imp\<close> then add_def_axiom
        else add_nondef_axiom) depth t
     and add_eq_axiom depth t =
       (if is_constr_pattern_formula ctxt t then add_def_axiom
@@ -1104,10 +1092,10 @@
   case t of
     (t0 as Const (\<^const_name>\<open>All\<close>, T0)) $ Abs (s, T1, t1) =>
     (case t1 of
-       (t10 as \<^const>\<open>HOL.conj\<close>) $ t11 $ t12 =>
+       (t10 as \<^Const_>\<open>conj\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+     | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>Ex\<close>, T0)
                                      $ Abs (s, T1, t11))
      | t1 =>
@@ -1117,14 +1105,14 @@
          t0 $ Abs (s, T1, distribute_quantifiers t1))
   | (t0 as Const (\<^const_name>\<open>Ex\<close>, T0)) $ Abs (s, T1, t1) =>
     (case distribute_quantifiers t1 of
-       (t10 as \<^const>\<open>HOL.disj\<close>) $ t11 $ t12 =>
+       (t10 as \<^Const_>\<open>disj\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>HOL.implies\<close>) $ t11 $ t12 =>
+     | (t10 as \<^Const_>\<open>implies\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
                                      $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+     | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
                                      $ Abs (s, T1, t11))
      | t1 =>
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Tue Sep 28 22:45:52 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 =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Sep 28 22:45:52 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} =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Tue Sep 28 22:45:52 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;
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 28 22:45:52 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>, _) =>
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Sep 28 22:45:52 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
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/conj_disj_perm.ML
--- a/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -25,9 +25,9 @@
 
 fun explode_thm thm =
   (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
-    \<^const>\<open>HOL.conj\<close> $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
-  | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm
-  | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ _) => explode_thm (thm RS @{thm notnotD})
+    \<^Const_>\<open>conj for _ _\<close> => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
+  | \<^Const_>\<open>Not for \<^Const_>\<open>disj for _ _\<close>\<close> => explode_conj_thm ndisj1_rule ndisj2_rule thm
+  | \<^Const_>\<open>Not for \<^Const_>\<open>Not for _\<close>\<close> => explode_thm (thm RS @{thm notnotD})
   | _ => add_lit thm)
 
 and explode_conj_thm rule1 rule2 thm lits =
@@ -36,7 +36,7 @@
 val not_false_rule = @{lemma "\<not>False" by auto}
 fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
 
-fun find_dual_lit lits (\<^const>\<open>HOL.Not\<close> $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
+fun find_dual_lit lits (\<^Const_>\<open>Not for t\<close>, thm) = Termtab.lookup lits t |> Option.map (pair thm)
   | find_dual_lit _ _ = NONE
 
 fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
@@ -49,10 +49,10 @@
     SOME thm => thm
   | NONE => join_term lits t)
 
-and join_term lits (\<^const>\<open>HOL.conj\<close> $ t $ u) = @{thm conjI} OF (map (join lits) [t, u])
-  | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t $ u)) =
+and join_term lits \<^Const_>\<open>conj for t u\<close> = @{thm conjI} OF (map (join lits) [t, u])
+  | join_term lits \<^Const_>\<open>Not for \<^Const_>\<open>HOL.disj for t u\<close>\<close> =
       ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u])
-  | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ t)) = join lits t RS not_not_rule
+  | join_term lits \<^Const_>\<open>Not for \<^Const>\<open>Not for t\<close>\<close> = join lits t RS not_not_rule
   | join_term _ t = raise TERM ("join_term", [t])
 
 fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu))
@@ -68,19 +68,19 @@
 
 fun prove_any_imp ct =
   (case Thm.term_of ct of
-    \<^const>\<open>HOL.False\<close> => @{thm FalseE}
-  | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.False\<close>) => not_not_false_rule
-  | \<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close> => not_true_rule
+    \<^Const_>\<open>False\<close> => @{thm FalseE}
+  | \<^Const_>\<open>Not for \<^Const>\<open>Not for \<^Const>\<open>False\<close>\<close>\<close> => not_not_false_rule
+  | \<^Const_>\<open>Not for \<^Const>\<open>True\<close>\<close> => not_true_rule
   | _ => raise CTERM ("prove_any_imp", [ct]))
 
 fun prove_contradiction_imp ct =
   with_assumption ct (fn thm =>
     let val lits = explode thm
     in
-      (case Termtab.lookup lits \<^const>\<open>HOL.False\<close> of
+      (case Termtab.lookup lits \<^Const>\<open>False\<close> of
         SOME thm' => thm' RS @{thm FalseE}
       | NONE =>
-          (case Termtab.lookup lits (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close>) of
+          (case Termtab.lookup lits \<^Const>\<open>Not for \<^Const>\<open>True\<close>\<close> of
             SOME thm' => thm' RS not_true_rule
           | NONE =>
               (case find_dual_lits lits of
@@ -99,13 +99,13 @@
 
 datatype kind = True | False | Conj | Disj | Other
 
-fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t
-  | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f
-  | choose _ _ c _ (\<^const>\<open>HOL.conj\<close> $ _ $ _) = c
-  | choose _ _ _ d (\<^const>\<open>HOL.disj\<close> $ _ $ _) = d
+fun choose t _ _ _ \<^Const_>\<open>True\<close> = t
+  | choose _ f _ _ \<^Const_>\<open>False\<close> = f
+  | choose _ _ c _ \<^Const_>\<open>conj for _ _\<close> = c
+  | choose _ _ _ d \<^Const_>\<open>disj for _ _\<close> = d
   | choose _ _ _ _ _ = Other
 
-fun kind_of (\<^const>\<open>HOL.Not\<close> $ t) = choose False True Disj Conj t
+fun kind_of \<^Const_>\<open>Not for t\<close> = choose False True Disj Conj t
   | kind_of t = choose True False Conj Disj t
 
 fun prove_conj_disj_perm ct cp =
@@ -120,7 +120,7 @@
 
 fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) => 
   (case Thm.term_of ct of
-    \<^const>\<open>HOL.Trueprop\<close> $ (@{const HOL.eq(bool)} $ _ $ _) =>
+    \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close>\<close> =>
       resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
   | _ => no_tac))
 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -31,7 +31,7 @@
 (** instantiate elimination rules **)
 
 local
-  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of \<^context> \<^const>\<open>False\<close>)
+  val (cpfalse, cfalse) = `SMT_Util.mk_cprop \<^cterm>\<open>False\<close>
 
   fun inst f ct thm =
     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -40,7 +40,7 @@
 
 fun instantiate_elim thm =
   (case Thm.concl_of thm of
-    \<^const>\<open>Trueprop\<close> $ Var (_, \<^typ>\<open>bool\<close>) => inst Thm.dest_arg cfalse thm
+    \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> => inst Thm.dest_arg cfalse thm
   | Var _ => inst I cpfalse thm
   | _ => thm)
 
@@ -51,9 +51,8 @@
 
 fun norm_def thm =
   (case Thm.prop_of thm of
-    \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) =>
-      norm_def (thm RS @{thm fun_cong})
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm)
+    \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close>\<close> => norm_def (thm RS @{thm fun_cong})
+  | \<^Const_>\<open>Pure.eq _ for _ \<open>Abs _\<close>\<close> => norm_def (HOLogic.mk_obj_eq thm)
   | _ => thm)
 
 
@@ -61,11 +60,11 @@
 
 fun atomize_conv ctxt ct =
   (case Thm.term_of ct of
-    \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
+    \<^Const_>\<open>Pure.imp for _ _\<close> =>
       Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
+  | \<^Const_>\<open>Pure.eq _ for _ _\<close> =>
       Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
-  | Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ =>
+  | \<^Const_>\<open>Pure.all _ for \<open>Abs _\<close>\<close> =>
       Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
   | _ => Conv.all_conv) ct
   handle CTERM _ => Conv.all_conv ct
@@ -120,9 +119,9 @@
 
   fun proper_quant inside f t =
     (case t of
-      Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => proper_quant true f u
-    | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => proper_quant true f u
-    | \<^const>\<open>trigger\<close> $ p $ u =>
+      \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+    | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+    | \<^Const_>\<open>trigger for p u\<close> =>
         (if inside then f p else false) andalso proper_quant false f u
     | Abs (_, _, u) => proper_quant false f u
     | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
@@ -142,7 +141,7 @@
   fun dest_cond_eq ct =
     (case Thm.term_of ct of
       Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Thm.dest_binop ct
-    | \<^const>\<open>HOL.implies\<close> $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
+    | \<^Const_>\<open>implies for _ _\<close> => dest_cond_eq (Thm.dest_arg ct)
     | _ => raise CTERM ("no equation", [ct]))
 
   fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
@@ -220,7 +219,7 @@
 
     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
 
-  fun has_trigger (\<^const>\<open>trigger\<close> $ _ $ _) = true
+  fun has_trigger \<^Const_>\<open>trigger for _ _\<close> = true
     | has_trigger _ = false
 
   fun try_trigger_conv cv ct =
@@ -331,12 +330,12 @@
 
 local
   val simple_nat_ops = [
-    @{const HOL.eq (nat)}, @{const less (nat)}, @{const less_eq (nat)},
-    \<^const>\<open>Suc\<close>, @{const plus (nat)}, @{const minus (nat)}]
+    \<^Const>\<open>HOL.eq \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less_eq \<^Type>\<open>nat\<close>\<close>,
+    \<^Const>\<open>Suc\<close>, \<^Const>\<open>plus \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>minus \<^Type>\<open>nat\<close>\<close>]
 
   val nat_consts = simple_nat_ops @
-    [@{const numeral (nat)}, @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] @
-    [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
+    [\<^Const>\<open>numeral \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>one_class.one \<^Type>\<open>nat\<close>\<close>] @
+    [\<^Const>\<open>times \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>divide \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>modulo \<^Type>\<open>nat\<close>\<close>]
 
   val is_nat_const = member (op aconv) nat_consts
 
@@ -349,10 +348,10 @@
 
   fun int_ops_conv cv ctxt ct =
     (case Thm.term_of ct of
-      @{const of_nat (int)} $ (Const (\<^const_name>\<open>If\<close>, _) $ _ $ _ $ _) =>
+      \<^Const_>\<open>of_nat \<^Type>\<open>int\<close> for \<open>\<^Const_>\<open>If _ for _ _ _\<close>\<close>\<close> =>
         Conv.rewr_conv int_if_thm then_conv
         if_conv (cv ctxt) (int_ops_conv cv ctxt)
-    | @{const of_nat (int)} $ _ =>
+    | \<^Const>\<open>of_nat \<^Type>\<open>int\<close> for _\<close> =>
         (Conv.rewrs_conv int_ops_thms then_conv
           Conv.top_sweep_conv (int_ops_conv cv) ctxt) else_conv
         Conv.arg_conv (Conv.sub_conv cv ctxt)
@@ -372,7 +371,7 @@
 
   fun add_int_of_nat vs ct cu (q, cts) =
     (case Thm.term_of ct of
-      @{const of_nat(int)} =>
+      \<^Const>\<open>of_nat \<^Type>\<open>int\<close>\<close> =>
         if Term.exists_subterm (member (op aconv) vs) (Thm.term_of cu) then (true, cts)
         else (q, insert (op aconvc) cu cts)
     | _ => (q, cts))
@@ -490,7 +489,7 @@
 
   val schematic_consts_of =
     let
-      fun collect (\<^const>\<open>trigger\<close> $ p $ t) = collect_trigger p #> collect t
+      fun collect \<^Const_>\<open>trigger for p t\<close> = collect_trigger p #> collect t
         | collect (t $ u) = collect t #> collect u
         | collect (Abs (_, _, t)) = collect t
         | collect (t as Const (n, _)) =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -25,7 +25,7 @@
     | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
     | is_linear _ = false
 
-  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
+  fun mk_times ts = Term.list_comb (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, ts)
 
   fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
 in
@@ -34,17 +34,17 @@
   SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
     (\<^typ>\<open>real\<close>, K (SOME ("Real", [])), real_num) #>
   fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
-    (@{const less (real)}, "<"),
-    (@{const less_eq (real)}, "<="),
-    (@{const uminus (real)}, "-"),
-    (@{const plus (real)}, "+"),
-    (@{const minus (real)}, "-") ] #>
+    (\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"),
+    (\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="),
+    (\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"),
+    (\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"),
+    (\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #>
   SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
-    (Term.dest_Const @{const times (real)}, times) #>
+    (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times) #>
   SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
-    (@{const times (real)}, "*") #>
+    (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #>
   SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
-    (@{const divide (real)}, "/")
+    (\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/")
 
 end
 
@@ -64,14 +64,14 @@
   fun mk_nary _ cu [] = cu
     | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
-  val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (real)})
-  val add = Thm.cterm_of \<^context> @{const plus (real)}
+  val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
+  val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
   val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0
-  val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (real)})
-  val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (real)})
-  val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> @{const divide (real)})
-  val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (real)})
-  val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (real)})
+  val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
+  val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
+  val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
+  val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
+  val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>
 
   fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smt_replay_methods.ML
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -218,30 +218,30 @@
 fun abstract_ter abs f t t1 t2 t3 =
   abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
 
-fun abstract_lit (\<^const>\<open>HOL.Not\<close> $ t) = abstract_term t #>> HOLogic.mk_not
+fun abstract_lit \<^Const>\<open>Not for t\<close> = abstract_term t #>> HOLogic.mk_not
   | abstract_lit t = abstract_term t
 
-fun abstract_not abs (t as \<^const>\<open>HOL.Not\<close> $ t1) =
+fun abstract_not abs (t as \<^Const_>\<open>Not\<close> $ t1) =
       abstract_sub t (abs t1 #>> HOLogic.mk_not)
   | abstract_not _ t = abstract_lit t
 
-fun abstract_conj (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun abstract_conj (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
       abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
   | abstract_conj t = abstract_lit t
 
-fun abstract_disj (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+fun abstract_disj (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
       abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
   | abstract_disj t = abstract_lit t
 
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+fun abstract_prop (t as (c as \<^Const>\<open>If \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 $ t3) =
       abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
-  | abstract_prop (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
-  | abstract_prop (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
-  | abstract_prop (t as \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>implies\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
-  | abstract_prop (t as \<^term>\<open>HOL.eq :: bool => _\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
   | abstract_prop t = abstract_not abstract_prop t
 
@@ -253,8 +253,8 @@
           abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
       | abs (t as (c as Const (\<^const_name>\<open>If\<close>, _)) $ t1 $ t2 $ t3) =
           abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
-      | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
-      | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+      | abs (t as \<^Const_>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+      | abs (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
       | abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
           abstract_sub t (abs t1 #>> (fn u => c $ u))
@@ -282,10 +282,10 @@
             | (NONE, _) => abstract_term t cx))
   in abs u end
 
-fun abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t1 $ t2))) =
+fun abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>disj for t1 t2\<close>\<close>) =
       abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
         HOLogic.mk_not o HOLogic.mk_disj)
-  | abstract_unit (t as (\<^const>\<open>HOL.disj\<close> $ t1 $ t2)) =
+  | abstract_unit (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
         HOLogic.mk_disj)
   | abstract_unit (t as (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) =
@@ -293,49 +293,49 @@
         abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2))) =
+  | abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close>) =
       if fastype_of t1 = \<^typ>\<open>bool\<close> then
         abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
           HOLogic.mk_eq #>> HOLogic.mk_not)
       else abstract_lit t
-  | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ t1)) =
+  | abstract_unit (t as \<^Const>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not)
   | abstract_unit t = abstract_lit t
 
-fun abstract_bool (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool (t as (@{const HOL.conj} $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const_>\<open>conj for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_conj)
-  | abstract_bool (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
       if fastype_of t1 = @{typ bool} then
         abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_bool (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool t1 #>> HOLogic.mk_not)
-  | abstract_bool (t as (@{const HOL.implies} $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const>\<open>implies for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_imp)
   | abstract_bool t = abstract_lit t
 
-fun abstract_bool_shallow (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool_shallow t1 ##>> abstract_bool_shallow t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool_shallow (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool_shallow (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool_shallow t1 #>> HOLogic.mk_not)
   | abstract_bool_shallow t = abstract_term t
 
-fun abstract_bool_shallow_equivalence (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow_equivalence (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool_shallow_equivalence t1 ##>> abstract_bool_shallow_equivalence t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool_shallow_equivalence (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
-      if fastype_of t1 = @{typ bool} then
+  | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
+      if fastype_of t1 = \<^Type>\<open>bool\<close> then
         abstract_sub t (abstract_lit t1 ##>> abstract_lit t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_bool_shallow_equivalence (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool_shallow_equivalence t1 #>> HOLogic.mk_not)
   | abstract_bool_shallow_equivalence t = abstract_lit t
 
@@ -347,8 +347,8 @@
           abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
       | abs (t as (Const (\<^const_name>\<open>If\<close>, _)) $ _ $ _ $ _) =
           abstract_sub t (abstract_term t)
-      | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
-      | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+      | abs (t as \<^Const>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+      | abs (t as \<^Const>\<open>disj\<close> $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
       | abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
           abstract_sub t (abs t1 #>> (fn u => c $ u))
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -306,12 +306,12 @@
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
       | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
       | (u, ts) => traverses Ts u ts)
-    and in_trigger Ts ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
+    and in_trigger Ts ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
       | in_trigger Ts t = traverse Ts t
     and in_pats Ts ps =
       in_list \<^typ>\<open>pattern symb_list\<close> (in_list \<^typ>\<open>pattern\<close> (in_pat Ts)) ps
-    and in_pat Ts ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) = p $ traverse Ts t
-      | in_pat Ts ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) = p $ traverse Ts t
+    and in_pat Ts ((p as \<^Const_>\<open>pat _\<close>) $ t) = p $ traverse Ts t
+      | in_pat Ts ((p as \<^Const_>\<open>nopat _\<close>) $ t) = p $ traverse Ts t
       | in_pat _ t = raise TERM ("bad pattern", [t])
     and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
   in map (traverse []) ts end
@@ -343,9 +343,9 @@
 
     fun in_term pat t =
       (case Term.strip_comb t of
-        (\<^const>\<open>True\<close>, []) => t
-      | (\<^const>\<open>False\<close>, []) => t
-      | (u as Const (\<^const_name>\<open>If\<close>, _), [t1, t2, t3]) =>
+        (\<^Const_>\<open>True\<close>, []) => t
+      | (\<^Const_>\<open>False\<close>, []) => t
+      | (u as \<^Const_>\<open>If _\<close>, [t1, t2, t3]) =>
           if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
       | (Const (c as (n, _)), ts) =>
           if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
@@ -364,7 +364,7 @@
     and in_pats ps =
       in_list \<^typ>\<open>pattern symb_list\<close> (SOME o in_list \<^typ>\<open>pattern\<close> (try in_pat)) ps
 
-    and in_trigger ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
+    and in_trigger ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
       | in_trigger t = in_form t
 
     and in_form t =
@@ -412,7 +412,7 @@
       | (ps, [false]) => cons (SNoPat ps)
       | _ => raise TERM ("bad multi-pattern", ts))
 
-fun dest_trigger (\<^const>\<open>trigger\<close> $ tl $ t) =
+fun dest_trigger \<^Const_>\<open>trigger for tl t\<close> =
       (rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t)
   | dest_trigger t = ([], t)
 
@@ -511,7 +511,7 @@
           |> (fn T => Const (\<^const_name>\<open>pat\<close>, T) $ lhs)
           |> SMT_Util.mk_symb_list \<^typ>\<open>pattern\<close> o single
           |> SMT_Util.mk_symb_list \<^typ>\<open>pattern symb_list\<close> o single
-          |> (fn t => \<^const>\<open>trigger\<close> $ t $ eq)
+          |> (fn t => \<^Const>\<open>trigger for t eq\<close>)
       | mk_trigger t = t
 
     val (ctxt2, (ts3, ll_defs)) =
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -131,16 +131,16 @@
 
 (* terms *)
 
-fun dest_conj (\<^const>\<open>HOL.conj\<close> $ t $ u) = (t, u)
+fun dest_conj \<^Const_>\<open>conj for t u\<close> = (t, u)
   | dest_conj t = raise TERM ("not a conjunction", [t])
 
-fun dest_disj (\<^const>\<open>HOL.disj\<close> $ t $ u) = (t, u)
+fun dest_disj \<^Const_>\<open>disj for t u\<close> = (t, u)
   | dest_disj t = raise TERM ("not a disjunction", [t])
 
 fun under_quant f t =
   (case t of
-    Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => under_quant f u
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => under_quant f u
+    \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
+  | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
   | _ => f t)
 
 val is_number =
@@ -197,17 +197,17 @@
 
 val dest_all_cbinders = repeat_yield (try o dest_cbinder)
 
-val mk_cprop = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Trueprop\<close>)
+val mk_cprop = Thm.apply \<^cterm>\<open>Trueprop\<close>
 
 fun dest_cprop ct =
   (case Thm.term_of ct of
-    \<^const>\<open>Trueprop\<close> $ _ => Thm.dest_arg ct
+    \<^Const_>\<open>Trueprop for _\<close> => Thm.dest_arg ct
   | _ => raise CTERM ("not a property", [ct]))
 
 val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
 
-val dest_prop = (fn \<^const>\<open>Trueprop\<close> $ t => t | t => t)
+val dest_prop = fn \<^Const_>\<open>Trueprop for t\<close> => t | t => t
 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)
 
@@ -237,7 +237,7 @@
 
 fun prop_conv cv ct =
   (case Thm.term_of ct of
-    \<^const>\<open>Trueprop\<close> $ _ => Conv.arg_conv cv ct
+    \<^Const_>\<open>Trueprop for _\<close> => Conv.arg_conv cv ct
   | _ => raise CTERM ("not a property", [ct]))
 
 end;
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -35,7 +35,7 @@
     | is_linear _ = false
 
   fun times _ _ ts =
-    let val mk = Term.list_comb o pair @{const times (int)}
+    let val mk = Term.list_comb o pair \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>
     in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
 in
 
@@ -46,21 +46,21 @@
     (\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
     (\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
-    (\<^const>\<open>True\<close>, "true"),
-    (\<^const>\<open>False\<close>, "false"),
-    (\<^const>\<open>Not\<close>, "not"),
-    (\<^const>\<open>HOL.conj\<close>, "and"),
-    (\<^const>\<open>HOL.disj\<close>, "or"),
-    (\<^const>\<open>HOL.implies\<close>, "=>"),
-    (@{const HOL.eq ('a)}, "="),
-    (@{const If ('a)}, "ite"),
-    (@{const less (int)}, "<"),
-    (@{const less_eq (int)}, "<="),
-    (@{const uminus (int)}, "-"),
-    (@{const plus (int)}, "+"),
-    (@{const minus (int)}, "-")] #>
+    (\<^Const>\<open>True\<close>, "true"),
+    (\<^Const>\<open>False\<close>, "false"),
+    (\<^Const>\<open>Not\<close>, "not"),
+    (\<^Const>\<open>conj\<close>, "and"),
+    (\<^Const>\<open>disj\<close>, "or"),
+    (\<^Const>\<open>implies\<close>, "=>"),
+    (\<^Const>\<open>HOL.eq \<^typ>\<open>'a\<close>\<close>, "="),
+    (\<^Const>\<open>If \<^typ>\<open>'a\<close>\<close>, "ite"),
+    (\<^Const>\<open>less \<^Type>\<open>int\<close>\<close>, "<"),
+    (\<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, "<="),
+    (\<^Const>\<open>uminus \<^Type>\<open>int\<close>\<close>, "-"),
+    (\<^Const>\<open>plus \<^Type>\<open>int\<close>\<close>, "+"),
+    (\<^Const>\<open>minus \<^Type>\<open>int\<close>\<close>, "-")] #>
   SMT_Builtin.add_builtin_fun smtlibC
-    (Term.dest_Const @{const times (int)}, times)
+    (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, times)
 
 end
 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/smtlib_proof.ML
--- a/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -150,8 +150,8 @@
 fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2
 fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2
 
-fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^const>\<open>HOL.True\<close>
-  | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^const>\<open>HOL.False\<close>
+fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^Const>\<open>True\<close>
+  | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^Const>\<open>False\<close>
   | core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t)
   | core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
   | core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -738,7 +738,7 @@
         fun remove_assumption_id assumption_id prems =
           filter_out (curry (op =) assumption_id) prems
         fun add_assumption assumption concl =
-          \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl
+          \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close>
         fun inline_assumption assumption assumption_id
             (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -38,8 +38,8 @@
      fp_kinds = [BNF_Util.Least_FP],
      serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
 
-  fun is_div_mod @{const divide (int)} = true
-    | is_div_mod @{const modulo (int)} = true
+  fun is_div_mod \<^Const_>\<open>divide \<^Type>\<open>int\<close>\<close> = true
+    | is_div_mod \<^Const>\<open>modulo \<^Type>\<open>int\<close>\<close> = true
     | is_div_mod _ = false
 
   val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
@@ -50,9 +50,9 @@
     else (thms, extra_thms)
 
   val setup_builtins =
-    SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
-    SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3div\<close>, "div") #>
-    SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3mod\<close>, "mod")
+    SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, "*") #>
+    SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3div\<close>, "div") #>
+    SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3mod\<close>, "mod")
 in
 
 val _ = Theory.setup (Context.theory_map (
@@ -116,13 +116,13 @@
   | mk_builtin_num ctxt i T =
       chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
 
-val mk_true = Thm.cterm_of \<^context> (\<^const>\<open>Not\<close> $ \<^const>\<open>False\<close>)
-val mk_false = Thm.cterm_of \<^context> \<^const>\<open>False\<close>
-val mk_not = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Not\<close>)
-val mk_implies = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>HOL.implies\<close>)
-val mk_iff = Thm.mk_binop (Thm.cterm_of \<^context> @{const HOL.eq (bool)})
-val conj = Thm.cterm_of \<^context> \<^const>\<open>HOL.conj\<close>
-val disj = Thm.cterm_of \<^context> \<^const>\<open>HOL.disj\<close>
+val mk_true = \<^cterm>\<open>\<not> False\<close>
+val mk_false = \<^cterm>\<open>False\<close>
+val mk_not = Thm.apply \<^cterm>\<open>HOL.Not\<close>
+val mk_implies = Thm.mk_binop \<^cterm>\<open>HOL.implies\<close>
+val mk_iff = Thm.mk_binop \<^cterm>\<open>(=) :: bool \<Rightarrow> _\<close>
+val conj = \<^cterm>\<open>HOL.conj\<close>
+val disj = \<^cterm>\<open>HOL.disj\<close>
 
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -143,15 +143,15 @@
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
   in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
 
-val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (int)})
-val add = Thm.cterm_of \<^context> @{const plus (int)}
+val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: int \<Rightarrow> _\<close>
+val add = \<^cterm>\<open>(+) :: int \<Rightarrow> _\<close>
 val int0 = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> 0
-val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3div\<close>)
-val mk_mod = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3mod\<close>)
-val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (int)})
+val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: int \<Rightarrow> _\<close>
+val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: int \<Rightarrow> _\<close>
+val mk_div = Thm.mk_binop \<^cterm>\<open>z3div\<close>
+val mk_mod = Thm.mk_binop \<^cterm>\<open>z3mod\<close>
+val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: int \<Rightarrow> _\<close>
+val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: int \<Rightarrow> _\<close>
 
 fun mk_builtin_fun ctxt sym cts =
   (case (sym, cts) of
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -315,10 +315,10 @@
   (thm COMP_INCR intro_hyp_rule1)
   handle THM _ => thm COMP_INCR intro_hyp_rule2
 
-fun negated_prop (\<^const>\<open>HOL.Not\<close> $ t) = HOLogic.mk_Trueprop t
+fun negated_prop \<^Const_>\<open>Not for t\<close> = HOLogic.mk_Trueprop t
   | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
 
-fun intro_hyps tab (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) cx =
+fun intro_hyps tab (t as \<^Const_>\<open>HOL.disj\<close> $ t1 $ t2) cx =
       lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
   | intro_hyps tab t cx =
       lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
@@ -376,7 +376,7 @@
 
 fun def_axiom_disj ctxt t =
   (case dest_prop t of
-    \<^const>\<open>HOL.disj\<close> $ u1 $ u2 =>
+    \<^Const_>\<open>disj for u1 u2\<close> =>
       SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
          SMT_Replay_Methods.abstract_prop u2 ##>>  SMT_Replay_Methods.abstract_prop u1 #>>
          HOLogic.mk_disj o swap)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -78,10 +78,10 @@
 
 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
 
-fun is_rec_def (\<^const>\<open>Trueprop\<close> $ t) = is_rec_def t
-  | is_rec_def (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = is_rec_def t2
-  | is_rec_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
-  | is_rec_def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
+fun is_rec_def \<^Const_>\<open>Trueprop for t\<close> = is_rec_def t
+  | is_rec_def \<^Const_>\<open>Pure.imp for _ t2\<close> = is_rec_def t2
+  | is_rec_def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = is_rec_eq t1 t2
+  | is_rec_def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = is_rec_eq t1 t2
   | is_rec_def _ = false
 
 fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms
@@ -249,8 +249,8 @@
       else
         Interesting
 
-    fun interest_of_prop _ (\<^const>\<open>Trueprop\<close> $ t) = interest_of_bool t
-      | interest_of_prop Ts (\<^const>\<open>Pure.imp\<close> $ t $ u) =
+    fun interest_of_prop _ \<^Const_>\<open>Trueprop for t\<close> = interest_of_bool t
+      | interest_of_prop Ts \<^Const_>\<open>Pure.imp for t u\<close> =
         combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
       | interest_of_prop Ts (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) =
         if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
@@ -331,9 +331,9 @@
       end
   end
 
-fun normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
+fun normalize_eq (\<^Const_>\<open>Trueprop\<close> $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
     if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
-  | normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as \<^const>\<open>Not\<close>
+  | normalize_eq (\<^Const_>\<open>Trueprop\<close> $ (t as \<^Const_>\<open>Not\<close>
       $ ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2))) =
     if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
   | normalize_eq (Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2) =
@@ -376,7 +376,7 @@
 
 fun struct_induct_rule_on th =
   (case Logic.strip_horn (Thm.prop_of th) of
-    (prems, \<^const>\<open>Trueprop\<close> $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
+    (prems, \<^Const_>\<open>Trueprop\<close> $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
     if not (is_TVar ind_T) andalso length prems > 1 andalso
        exists (exists_subterm (curry (op aconv) p)) prems andalso
        not (exists (exists_subterm (curry (op aconv) a)) prems) then
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -178,18 +178,18 @@
     and do_formula t =
       (case t of
         Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t') => do_formula t'
-      | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
+      | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_formula t1 #> do_formula t2
       | Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
         do_term_or_formula false T t1 #> do_term_or_formula true T t2
-      | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1
-      | \<^const>\<open>False\<close> => I
-      | \<^const>\<open>True\<close> => I
-      | \<^const>\<open>Not\<close> $ t1 => do_formula t1
+      | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1
+      | \<^Const_>\<open>False\<close> => I
+      | \<^Const_>\<open>True\<close> => I
+      | \<^Const_>\<open>Not for t1\<close> => do_formula t1
       | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => do_formula t'
       | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => do_formula t'
-      | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
-      | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
-      | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
+      | \<^Const_>\<open>conj for t1 t2\<close> => do_formula t1 #> do_formula t2
+      | \<^Const_>\<open>disj for t1 t2\<close> => do_formula t1 #> do_formula t2
+      | \<^Const_>\<open>implies for t1 t2\<close> => do_formula t1 #> do_formula t2
       | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
         do_term_or_formula false T t1 #> do_term_or_formula true T t2
       | Const (\<^const_name>\<open>If\<close>, Type (_, [_, Type (_, [T, _])])) $ t1 $ t2 $ t3 =>
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -76,17 +76,17 @@
     fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
     fun do_formula pos t =
       (case (pos, t) of
-        (_, \<^const>\<open>Trueprop\<close> $ t1) => do_formula pos t1
+        (_, \<^Const_>\<open>Trueprop for t1\<close>) => do_formula pos t1
       | (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
       | (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
       | (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
-      | (_, \<^const>\<open>Pure.imp\<close> $ t1 $ t2) =>
+      | (_, \<^Const_>\<open>Pure.imp for t1 t2\<close>) =>
         do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2)
-      | (_, \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =>
-        do_formula (not pos) t1 andalso (t2 = \<^const>\<open>False\<close> orelse do_formula pos t2)
-      | (_, \<^const>\<open>Not\<close> $ t1) => do_formula (not pos) t1
-      | (true, \<^const>\<open>HOL.disj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
-      | (false, \<^const>\<open>HOL.conj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+      | (_, \<^Const_>\<open>implies for t1 t2\<close>) =>
+        do_formula (not pos) t1 andalso (t2 = \<^Const>\<open>False\<close> orelse do_formula pos t2)
+      | (_, \<^Const_>\<open>Not for t1\<close>) => do_formula (not pos) t1
+      | (true, \<^Const_>\<open>disj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
+      | (false, \<^Const_>\<open>conj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
       | (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
       | (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
       | _ => false)
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 28 22:45:52 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
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/etc/options	Tue Sep 28 22:45:52 2021 +0200
@@ -26,7 +26,7 @@
 
 section "Miscellaneous Tools"
 
-public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
+public option sledgehammer_provers : string = "cvc4 z3 spass e vampire"
   -- "provers for Sledgehammer (separated by blanks)"
 
 public option sledgehammer_timeout : int = 30
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/record.ML	Tue Sep 28 22:45:52 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))
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Sep 28 22:45:52 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) 
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 28 22:45:52 2021 +0200
@@ -1289,7 +1289,7 @@
 
   fun decomp \<^Const_>\<open>Trueprop for t\<close> =
         let
-          fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
+          fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
               let
                 fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
                   | decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")
diff -r 90c99974f648 -r bd9a5e128c31 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/HOL/Typerep.thy	Tue Sep 28 22:45:52 2021 +0200
@@ -32,7 +32,7 @@
 
 typed_print_translation \<open>
   let
-    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
+    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<^Type>\<open>itself T\<close> _\<close>
             (Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
           Term.list_comb
             (Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/General/antiquote.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -7,6 +7,8 @@
 signature ANTIQUOTE =
 sig
   type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
+  val no_control: control
+  val control_symbols: control -> Symbol_Pos.T list
   type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
   val is_text: 'a antiquote -> bool
@@ -17,7 +19,8 @@
   val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: 'a antiquote list -> Position.report list
   val update_reports: bool -> Position.T -> string list -> Position.report_text list
-  val scan_control: control scanner
+  val err_prefix: string
+  val scan_control: string -> control scanner
   val scan_antiq: antiq scanner
   val scan_antiquote: text_antiquote scanner
   val scan_antiquote_comments: text_antiquote scanner
@@ -31,6 +34,10 @@
 (* datatype antiquote *)
 
 type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
+val no_control = {range = Position.no_range, name = ("", Position.none), body = []};
+fun control_symbols ({name = (name, pos), body, ...}: control) =
+  (Symbol.encode (Symbol.Control name), pos) :: body;
+
 type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
 datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
 
@@ -112,9 +119,9 @@
 
 open Basic_Symbol_Pos;
 
-local
+val err_prefix = "Antiquotation lexical error: ";
 
-val err_prefix = "Antiquotation lexical error: ";
+local
 
 val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
 val scan_nl_opt = Scan.optional scan_nl [];
@@ -148,9 +155,9 @@
 
 in
 
-val scan_control =
+fun scan_control err =
   Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
-  Symbol_Pos.scan_cartouche err_prefix >>
+  Symbol_Pos.scan_cartouche err >>
     (fn (opt_control, body) =>
       let
         val (name, range) =
@@ -173,10 +180,10 @@
        body = body});
 
 val scan_antiquote =
-  scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
+  scan_text >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
 
 val scan_antiquote_comments =
-  scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
+  scan_text_comments >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
 
 end;
 
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/General/scan.scala	Tue Sep 28 22:45:52 2021 +0200
@@ -290,6 +290,13 @@
     }
 
 
+    /* control cartouches */
+
+    val control_symbol: Parser[String] = one(Symbol.is_control)
+
+    val control_cartouche: Parser[String] = control_symbol ~ cartouche ^^ { case a ~ b => a + b }
+
+
     /* keyword */
 
     def literal(lexicon: Lexicon): Parser[String] = new Parser[String]
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -32,6 +32,7 @@
   val alt_string: string parser
   val verbatim: string parser
   val cartouche: string parser
+  val control: Antiquote.control parser
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
@@ -195,6 +196,7 @@
 val alt_string = kind Token.Alt_String;
 val verbatim = kind Token.Verbatim;
 val cartouche = kind Token.Cartouche;
+val control = token (kind Token.control_kind) >> (the o Token.get_control);
 val eof = kind Token.EOF;
 
 fun command_name x =
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/Isar/token.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -11,9 +11,12 @@
     Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
     Float | Space |
     (*delimited content*)
-    String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+    String | Alt_String | Verbatim | Cartouche |
+    Control of Antiquote.control |
+    Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
+  val control_kind: kind
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
@@ -37,6 +40,7 @@
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
+  val get_control: T -> Antiquote.control option
   val is_command: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
   val is_command_modifier: T -> bool
@@ -118,10 +122,20 @@
   Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
   Float | Space |
   (*delimited content*)
-  String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+  String | Alt_String | Verbatim | Cartouche |
+  Control of Antiquote.control |
+  Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
 
+val control_kind = Control Antiquote.no_control;
+
+fun equiv_kind kind kind' =
+  (case (kind, kind') of
+    (Control _, Control _) => true
+  | (Error _, Error _) => true
+  | _ => kind = kind');
+
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
@@ -138,6 +152,7 @@
   | Alt_String => "back-quoted string"
   | Verbatim => "verbatim text"
   | Cartouche => "text cartouche"
+  | Control _ => "control cartouche"
   | Comment NONE => "informal comment"
   | Comment (SOME _) => "formal comment"
   | Error _ => "bad input"
@@ -152,6 +167,7 @@
     | Alt_String => true
     | Verbatim => true
     | Cartouche => true
+    | Control _ => true
     | Comment _ => true
     | _ => false);
 
@@ -214,7 +230,10 @@
 (* kind of token *)
 
 fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
+fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k';
+
+fun get_control tok =
+  (case kind_of tok of Control control => SOME control | _ => NONE);
 
 val is_command = is_kind Command;
 
@@ -304,6 +323,7 @@
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
+  | Control _ => (Markup.cartouche, "")
   | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
@@ -354,6 +374,7 @@
   | Alt_String => Symbol_Pos.quote_string_bq x
   | Verbatim => enclose "{*" "*}" x
   | Cartouche => cartouche x
+  | Control control => Symbol_Pos.content (Antiquote.control_symbols control)
   | Comment NONE => enclose "(*" "*)" x
   | EOF => ""
   | _ => x);
@@ -646,9 +667,11 @@
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_verbatim >> token_range Verbatim ||
-    scan_cartouche >> token_range Cartouche ||
     scan_comment >> token_range (Comment NONE) ||
     Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
+    scan_cartouche >> token_range Cartouche ||
+    Antiquote.scan_control err_prefix >> (fn control =>
+      token (Control control) (Antiquote.control_symbols control)) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/Isar/token.scala	Tue Sep 28 22:45:52 2021 +0200
@@ -34,6 +34,7 @@
     val ALT_STRING = Value("back-quoted string")
     val VERBATIM = Value("verbatim text")
     val CARTOUCHE = Value("text cartouche")
+    val CONTROL = Value("control cartouche")
     val INFORMAL_COMMENT = Value("informal comment")
     val FORMAL_COMMENT = Value("formal comment")
     /*special content*/
@@ -53,11 +54,12 @@
       val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
       val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
       val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
-      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
       val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
       val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
+      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
+      val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
 
-      string | (alt_string | (verb | (cart | (cmt | formal_cmt))))
+      string | (alt_string | (verb | (cmt | (formal_cmt | (cart | ctrl)))))
     }
 
     private def other_token(keywords: Keyword.Keywords): Parser[Token] =
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -234,27 +234,35 @@
     | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
   end;
 
-fun ml_sources ctxt srcs =
+fun ml_args ctxt args =
   let
-    val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes o ML_Lex.read_source) srcs ctxt;
+    val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes) args ctxt;
     fun decl' ctxt'' = map (fn decl => decl ctxt'') decls;
   in (decl', ctxt') end
 
 val parse_name = Parse.input Parse.name;
-val parse_args = Scan.repeat (Parse.input Parse.underscore || Parse.embedded_input);
+
+val parse_arg =
+  Parse.input Parse.underscore >> ML_Lex.read_source ||
+  Parse.embedded_input >> ML_Lex.read_source ||
+  Parse.control >> (ML_Lex.read_symbols o Antiquote.control_symbols);
+
+val parse_args = Scan.repeat parse_arg;
 val parse_for_args =
   Scan.optional ((Parse.position (Parse.$$$ "for") >> #2) -- Parse.!!! parse_args)
     (Position.none, []);
 
 fun parse_body b =
-  if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> single
+  if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single)
   else Scan.succeed [];
 
-fun is_dummy s = Input.string_of s = "_";
+fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_"
+  | is_dummy _ = false;
 
 val ml = ML_Lex.tokenize_no_range;
 val ml_range = ML_Lex.tokenize_range;
 val ml_dummy = ml "_";
+fun ml_enclose range x = ml_range range "(" @ x @ ml_range range ")";
 fun ml_parens x = ml "(" @ x @ ml ")";
 fun ml_bracks x = ml "[" @ x @ ml "]";
 fun ml_commas xs = flat (separate (ml ", ") xs);
@@ -279,18 +287,20 @@
             error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^
               " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos);
 
-        val (decls1, ctxt1) = ml_sources ctxt type_args;
-        val (decls2, ctxt2) = (ml_sources ctxt1) fn_body;
+        val (decls1, ctxt1) = ml_args ctxt type_args;
+        val (decls2, ctxt2) = ml_args ctxt1 fn_body;
         fun decl' ctxt' =
           let
             val (ml_args_env, ml_args_body) = split_list (decls1 ctxt');
             val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt');
-            val ml1 = ml_parens (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body));
+            val ml1 =
+              ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body));
             val ml2 =
               if function then
-                ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
-                ml "| T => " @ ml_range range "raise" @
-                ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], []))"
+                ml_enclose range
+                 (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
+                  ml "| T => " @ ml_range range "raise" @
+                  ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])")
               else ml1;
           in (flat (ml_args_env @ ml_fn_env), ml2) end;
       in (decl', ctxt2) end);
@@ -321,11 +331,11 @@
           length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
         val _ =
           length term_args > m andalso Term.is_Type (Term.body_type T) andalso
-            err (" cannot have more than " ^ string_of_int m ^ " type argument(s)");
+            err (" cannot have more than " ^ string_of_int m ^ " argument(s)");
 
-        val (decls1, ctxt1) = ml_sources ctxt type_args;
-        val (decls2, ctxt2) = ml_sources ctxt1 term_args;
-        val (decls3, ctxt3) = ml_sources ctxt2 fn_body;
+        val (decls1, ctxt1) = ml_args ctxt type_args;
+        val (decls2, ctxt2) = ml_args ctxt1 term_args;
+        val (decls3, ctxt3) = ml_args ctxt2 fn_body;
         fun decl' ctxt' =
           let
             val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt');
@@ -351,12 +361,13 @@
               | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u);
 
             val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env);
-            val ml1 = ml_parens (ml_app (rev ml_args_body2));
+            val ml1 = ml_enclose range (ml_app (rev ml_args_body2));
             val ml2 =
               if function then
-                ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
-                ml "| t => " @ ml_range range "raise" @
-                ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t]))"
+                ml_enclose range
+                 (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
+                  ml "| t => " @ ml_range range "raise" @
+                  ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])")
               else ml1;
           in (ml_env, ml2) end;
       in (decl', ctxt3) end);
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -36,6 +36,7 @@
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
   val read_source_sml: Input.source -> token Antiquote.antiquote list
+  val read_symbols: Symbol_Pos.T list -> token Antiquote.antiquote list
   val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
 end;
 
@@ -315,7 +316,7 @@
 
 val scan_ml_antiq =
   Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
-  Antiquote.scan_control >> Antiquote.Control ||
+  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
   scan_rat_antiq >> Antiquote.Antiq ||
   scan_sml_antiq;
@@ -389,6 +390,7 @@
   read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
     scan_sml_antiq;
 
+val read_symbols = reader {opaque_warning = true} scan_ml_antiq;
 val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
 
 end;
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/Thy/document_output.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -156,6 +156,7 @@
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
     | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
     | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
+    | Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
diff -r 90c99974f648 -r bd9a5e128c31 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Pure/Tools/generated_files.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -201,7 +201,7 @@
   end;
 
 val scan_antiq =
-  Antiquote.scan_control >> Antiquote.Control ||
+  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
 
 fun read_source ctxt (file_type: file_type) source =
diff -r 90c99974f648 -r bd9a5e128c31 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 28 22:45:52 2021 +0200
@@ -72,6 +72,7 @@
       Token.Kind.ALT_STRING -> LITERAL2,
       Token.Kind.VERBATIM -> COMMENT3,
       Token.Kind.CARTOUCHE -> COMMENT3,
+      Token.Kind.CONTROL -> COMMENT3,
       Token.Kind.INFORMAL_COMMENT -> COMMENT1,
       Token.Kind.FORMAL_COMMENT -> COMMENT1,
       Token.Kind.ERROR -> INVALID
diff -r 90c99974f648 -r bd9a5e128c31 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -298,7 +298,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_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
+     fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close>, iprems) =
           (case AList.lookup (op aconv) ind_alist X of
                SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -391,7 +391,7 @@
                             elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
              fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
-               \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
+               \<^Const>\<open>imp for \<^Const>\<open>mem for elem_tuple rec_tm\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
        in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
@@ -400,7 +400,7 @@
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
+         \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> \<open>pred $ Bound 0\<close>\<close>;
 
      (*To instantiate the main induction rule*)
      val induct_concl =
diff -r 90c99974f648 -r bd9a5e128c31 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -76,7 +76,7 @@
          if length rls <= maxr then resolve_tac ctxt rls i else no_tac
       end);
 
-fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for a _\<close>\<close> = not (is_Var (head_of a))
   | is_rigid_elem _ = false;
 
 (*Try solving a:A by assumption provided a is rigid!*)
diff -r 90c99974f648 -r bd9a5e128c31 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/ZF/arith_data.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -48,7 +48,7 @@
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =
   if fastype_of t = \<^Type>\<open>i\<close>
-  then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+  then \<^Const>\<open>IFOL.eq \<^Type>\<open>i\<close> for t u\<close>
   else \<^Const>\<open>IFOL.iff for t u\<close>;
 
 (*We remove equality assumptions because they confuse the simplifier and
diff -r 90c99974f648 -r bd9a5e128c31 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Sep 28 20:58:04 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Sep 28 22:45:52 2021 +0200
@@ -22,7 +22,7 @@
 fun mk_all_imp (A,P) =
   let val T = \<^Type>\<open>i\<close> in
     \<^Const>\<open>All T for
-      \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
+      \<open>Abs ("v", T, \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
   end;
 
 fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
@@ -37,7 +37,7 @@
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl =
-    let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
+    let val \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close> = Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)