# HG changeset patch
# User wenzelm
# Date 1632859731 -7200
# Node ID 9ea507f63bcb62633892592a08a42b39064fcf73
# Parent  bb25ea271b159b75b93bd811a554cdcb8b03334d
clarified antiquotations;

diff -r bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Sep 28 22:08:51 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 bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Sep 28 22:08:51 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 bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Sep 28 22:08:51 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 bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 28 22:08:51 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 bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Sep 28 22:08:51 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 bb25ea271b15 -r 9ea507f63bcb src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 28 22:08:51 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)