# HG changeset patch
# User wenzelm
# Date 1632860042 -7200
# Node ID 8d0294d877bd47b1890cb3acf1507b216ac24b77
# Parent  79f484b0e35ba656f9e6e536331ed58c9dfef86e
clarified antiquotations;

diff -r 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/conj_disj_perm.ML
--- a/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smt_replay_methods.ML
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/smtlib_proof.ML
--- a/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Sep 28 22:14:02 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 79f484b0e35b -r 8d0294d877bd src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 22:14:02 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)