# HG changeset patch
# User wenzelm
# Date 1632948878 -7200
# Node ID e80c4cde606476ac666ede7749ce2d9213530639
# Parent  dc73f9e6476b8758914517c4d02592b1e103e5e8
clarified antiquotations;
some comments concerning odd "- numeral";

diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -1033,24 +1033,24 @@
         form
     } ctxt ct
 
-  fun term_of_bool true = \<^term>\<open>True\<close>
-    | term_of_bool false = \<^term>\<open>False\<close>;
+  fun term_of_bool true = \<^Const>\<open>True\<close>
+    | term_of_bool false = \<^Const>\<open>False\<close>;
 
-  val mk_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+  val mk_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
 
   fun term_of_float (@{code Float} (k, l)) =
-    \<^term>\<open>Float\<close> $ mk_int k $ mk_int l;
+    \<^Const>\<open>Float for \<open>mk_int k\<close> \<open>mk_int l\<close>\<close>;
 
   fun term_of_float_interval x = @{term "Interval::_\<Rightarrow>float interval"} $
     HOLogic.mk_prod
       (apply2 term_of_float (@{code lowerF} x, @{code upperF} x))
 
-  fun term_of_float_interval_option NONE = \<^term>\<open>None :: (float interval) option\<close>
-    | term_of_float_interval_option (SOME ff) = \<^term>\<open>Some :: float interval \<Rightarrow> _\<close>
-        $ (term_of_float_interval ff);
+  fun term_of_float_interval_option NONE = \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close>
+    | term_of_float_interval_option (SOME ff) =
+        \<^Const>\<open>Some \<^typ>\<open>float interval\<close> for \<open>term_of_float_interval ff\<close>\<close>;
 
   val term_of_float_interval_option_list =
-    HOLogic.mk_list \<^typ>\<open>(float interval) option\<close> o map term_of_float_interval_option;
+    HOLogic.mk_list \<^typ>\<open>float interval option\<close> o map term_of_float_interval_option;
 
   val approx_bool = @{computation bool}
     (fn _ => fn x => case x of SOME b => term_of_bool b
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -649,13 +649,13 @@
   by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
 
 ML \<open>
-val term_of_nat = HOLogic.mk_number \<^typ>\<open>nat\<close> o @{code integer_of_nat};
+val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
 
-val term_of_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
 
-fun term_of_pol (@{code Pc} k) = \<^term>\<open>Pc\<close> $ term_of_int k
-  | term_of_pol (@{code Pinj} (n, p)) = \<^term>\<open>Pinj\<close> $ term_of_nat n $ term_of_pol p
-  | term_of_pol (@{code PX} (p, n, q)) = \<^term>\<open>PX\<close> $ term_of_pol p $ term_of_nat n $ term_of_pol q;
+fun term_of_pol (@{code Pc} k) = \<^Const>\<open>Pc\<close> $ term_of_int k
+  | term_of_pol (@{code Pinj} (n, p)) = \<^Const>\<open>Pinj\<close> $ term_of_nat n $ term_of_pol p
+  | term_of_pol (@{code PX} (p, n, q)) = \<^Const>\<open>PX\<close> $ term_of_pol p $ term_of_nat n $ term_of_pol q;
 
 local
 
@@ -742,53 +742,43 @@
        in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
    | NONE => error "get_ring_simps: lookup failed");
 
-fun ring_struct (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ R $ _ $ _) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ R $ _ $ _) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ R $ _ $ _) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ R $ _) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Group.pow\<close>, _) $ R $ _ $ _) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ R) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ R) = SOME R
-  | ring_struct (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ R $ _) = SOME R
+fun ring_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
+  | ring_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
   | ring_struct _ = NONE;
 
-fun reif_polex vs (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>Add\<close> $ reif_polex vs a $ reif_polex vs b
-  | reif_polex vs (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>Sub\<close> $ reif_polex vs a $ reif_polex vs b
-  | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>Mul\<close> $ reif_polex vs a $ reif_polex vs b
-  | reif_polex vs (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ _ $ a) =
-      \<^const>\<open>Neg\<close> $ reif_polex vs a
-  | reif_polex vs (Const (\<^const_name>\<open>Group.pow\<close>, _) $ _ $ a $ n) =
-      \<^const>\<open>Pow\<close> $ reif_polex vs a $ n
+fun reif_polex vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
+      \<^Const>\<open>Add for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+  | reif_polex vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
+      \<^Const>\<open>Sub for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+  | reif_polex vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
+      \<^Const>\<open>Mul for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+  | reif_polex vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
+      \<^Const>\<open>Neg for \<open>reif_polex vs a\<close>\<close>
+  | reif_polex vs \<^Const_>\<open>Group.pow _ _ _ for _ a n\<close> =
+      \<^Const>\<open>Pow for \<open>reif_polex vs a\<close> n\<close>
   | reif_polex vs (Free x) =
-      \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
-  | reif_polex vs (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ _) =
-      \<^term>\<open>Const 0\<close>
-  | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ _) =
-      \<^term>\<open>Const 1\<close>
-  | reif_polex vs (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ _ $ n) =
-      \<^const>\<open>Const\<close> $ n
+      \<^Const>\<open>Var for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+  | reif_polex _ \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>Const 0\<close>
+  | reif_polex _ \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>Const 1\<close>
+  | reif_polex _ \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>Const for n\<close>
   | reif_polex _ _ = error "reif_polex: bad expression";
 
-fun reif_polex' vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
-      \<^const>\<open>Add\<close> $ reif_polex' vs a $ reif_polex' vs b
-  | reif_polex' vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
-      \<^const>\<open>Sub\<close> $ reif_polex' vs a $ reif_polex' vs b
-  | reif_polex' vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
-      \<^const>\<open>Mul\<close> $ reif_polex' vs a $ reif_polex' vs b
-  | reif_polex' vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ a) =
-      \<^const>\<open>Neg\<close> $ reif_polex' vs a
-  | reif_polex' vs (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
-      \<^const>\<open>Pow\<close> $ reif_polex' vs a $ n
-  | reif_polex' vs (Free x) =
-      \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
-  | reif_polex' vs (Const (\<^const_name>\<open>numeral\<close>, _) $ b) =
-      \<^const>\<open>Const\<close> $ (@{const numeral (int)} $ b)
-  | reif_polex' vs (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = \<^term>\<open>Const 0\<close>
-  | reif_polex' vs (Const (\<^const_name>\<open>one_class.one\<close>, _)) = \<^term>\<open>Const 1\<close>
-  | reif_polex' vs t = error "reif_polex: bad expression";
+fun reif_polex' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>Add for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+  | reif_polex' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>Sub for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+  | reif_polex' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>Mul for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+  | reif_polex' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>Neg for \<open>reif_polex' vs a\<close>\<close>
+  | reif_polex' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>Pow for \<open>reif_polex' vs a\<close> n\<close>
+  | reif_polex' vs (Free x) = \<^Const>\<open>Var for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> (find_index (equal x) vs)\<close>\<close>
+  | reif_polex' _ \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>Const for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
+  | reif_polex' _ \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>Const 0\<close>
+  | reif_polex' _ \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>Const 1\<close>
+  | reif_polex' _ t = error "reif_polex: bad expression";
 
 fun head_conv (_, _, _, _, head_simp, _) ys =
   (case strip_app ys of
@@ -892,9 +882,8 @@
     val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
     val ths = map (fn p as (x, _) =>
       (case find_first
-         ((fn Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                (Const (\<^const_name>\<open>Set.member\<close>, _) $
-                   Free (y, _) $ (Const (\<^const_name>\<open>carrier\<close>, _) $ S)) =>
+         ((fn \<^Const_>\<open>Trueprop
+              for \<^Const_>\<open>Set.member _ for \<open>Free (y, _)\<close> \<^Const_>\<open>carrier _ _ for S\<close>\<close>\<close> =>
                 x = y andalso R aconv S
             | _ => false) o Thm.prop_of) props of
          SOME th => th
@@ -905,11 +894,7 @@
        ths in_carrier_Nil
   end;
 
-fun mk_ring T =
-  Const (\<^const_name>\<open>cring_class_ops\<close>,
-    Type (\<^type_name>\<open>partial_object_ext\<close>, [T,
-      Type (\<^type_name>\<open>monoid_ext\<close>, [T,
-        Type (\<^type_name>\<open>ring_ext\<close>, [T, \<^typ>\<open>unit\<close>])])]));
+fun mk_ring T = \<^Const>\<open>cring_class_ops T\<close>;
 
 val iterations = \<^cterm>\<open>1000::nat\<close>;
 val Trueprop_cong = Thm.combination (Thm.reflexive \<^cterm>\<open>Trueprop\<close>);
@@ -926,7 +911,7 @@
       | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
     val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
     val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
-    val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\<open>polex * polex\<close>
+    val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\<open>polex \<times> polex\<close>
       (map (HOLogic.mk_prod o apply2 reif) eqs'));
     val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
     val prem = Thm.equal_elim
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Conversions.thy
--- a/src/HOL/Decision_Procs/Conversions.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Conversions.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -257,13 +257,12 @@
   in
     fn n =>
       case Thm.term_of n of
-        Const (\<^const_name>\<open>one_class.one\<close>, _) => numeral_1_eq_1_a
-      | Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) =>
+        \<^Const_>\<open>one_class.one _\<close> => numeral_1_eq_1_a
+      | \<^Const_>\<open>uminus _ for \<^Const_>\<open>one_class.one _\<close>\<close> =>
           Thm.combination (Thm.reflexive (Thm.dest_fun n)) numeral_1_eq_1_a
-      | Const (\<^const_name>\<open>zero_class.zero\<close>, _) => Thm.reflexive n
-      | Const (\<^const_name>\<open>numeral\<close>, _) $ _ => Thm.reflexive n
-      | Const (\<^const_name>\<open>uminus\<close>, _) $
-          (Const (\<^const_name>\<open>numeral\<close>, _) $ _) => Thm.reflexive n
+      | \<^Const_>\<open>zero_class.zero _\<close> => Thm.reflexive n
+      | \<^Const_>\<open>numeral _ for _\<close> => Thm.reflexive n
+      | \<^Const_>\<open>uminus _ for \<^Const_>\<open>numeral _ for _\<close>\<close> => Thm.reflexive n
       | _ => err "expand1" n
   end;
 
@@ -272,10 +271,8 @@
   in
     fn eq =>
       case Thm.term_of (Thm.rhs_of eq) of
-        Const (\<^const_name>\<open>Num.numeral\<close>, _) $ Const (\<^const_name>\<open>Num.One\<close>, _) =>
-          Thm.transitive eq numeral_1_eq_1_a
-      | Const (\<^const_name>\<open>uminus\<close>, _) $
-          (Const (\<^const_name>\<open>Num.numeral\<close>, _) $ Const (\<^const_name>\<open>Num.One\<close>, _)) =>
+        \<^Const_>\<open>Num.numeral _ for \<^Const_>\<open>Num.One\<close>\<close> => Thm.transitive eq numeral_1_eq_1_a
+      | \<^Const_>\<open>uminus _ for \<^Const_>\<open>Num.numeral _ for \<^Const_>\<open>Num.One\<close>\<close>\<close> =>
             Thm.transitive eq
               (Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.rhs_of eq)))
                  numeral_1_eq_1_a)
@@ -777,7 +774,7 @@
             val eq = Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.dest_fun2 ct))) p_eq
           in
             case Thm.term_of (Thm.rhs_of p_eq) of
-              Const (\<^const_name>\<open>True\<close>, _) =>
+              \<^Const_>\<open>True\<close> =>
                 let
                   val x_eq = x cx;
                   val cx = Thm.rhs_of x_eq;
@@ -788,7 +785,7 @@
                        (Thm.reflexive cy))
                     (inst [] [cx, cy] if_True)
                 end
-            | Const (\<^const_name>\<open>False\<close>, _) =>
+            | \<^Const_>\<open>False\<close> =>
                 let
                   val y_eq = y cy;
                   val cy = Thm.rhs_of y_eq;
@@ -812,7 +809,7 @@
     val If_conv_a = If_conv (type_of_eqn drop_0_a);
 
     fun conv n ys = (case Thm.term_of n of
-        Const (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [ys] drop_0_a
+        \<^Const_>\<open>zero_class.zero _\<close> => inst [] [ys] drop_0_a
       | _ => (case strip_app ys of
           (\<^const_name>\<open>Cons\<close>, [x, xs]) =>
             transitive'
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -2386,17 +2386,17 @@
   | num_of_term vs \<^term>\<open>0::int\<close> = @{code C} (@{code int_of_integer} 0)
   | num_of_term vs \<^term>\<open>1::int\<close> = @{code C} (@{code int_of_integer} 1)
   | num_of_term vs \<^term>\<open>- 1::int\<close> = @{code C} (@{code int_of_integer} (~ 1))
-  | num_of_term vs (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t) =
+  | num_of_term vs \<^Const_>\<open>numeral _ for t\<close> =
       @{code C} (@{code int_of_integer} (HOLogic.dest_numeral t))
-  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t) =
+  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t) =  (* FIXME !? *)
       @{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t)))
   | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
-  | num_of_term vs (\<^term>\<open>uminus :: int \<Rightarrow> int\<close> $ t') = @{code Neg} (num_of_term vs t')
-  | num_of_term vs (\<^term>\<open>(+) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+  | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>int\<close> for t1 t2\<close> =
       @{code Add} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(-) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>int\<close> for t1 t2\<close> =
       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(*) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>int\<close> for t1 t2\<close> =
       (case try HOLogic.dest_number t1 of
         SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
       | NONE =>
@@ -2405,34 +2405,34 @@
           | NONE => error "num_of_term: unsupported multiplication"))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term \<^context> t);
 
-fun fm_of_term ps vs \<^term>\<open>True\<close> = @{code T}
-  | fm_of_term ps vs \<^term>\<open>False\<close> = @{code F}
-  | fm_of_term ps vs (\<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term ps vs \<^Const_>\<open>True\<close> = @{code T}
+  | fm_of_term ps vs \<^Const_>\<open>False\<close> = @{code F}
+  | fm_of_term ps vs \<^Const_>\<open>less \<^Type>\<open>int\<close> for t1 t2\<close> =
       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term ps vs (\<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>less_eq \<^Type>\<open>int\<close> for t1 t2\<close> =
       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term ps vs (\<^term>\<open>(=) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.eq \<^Type>\<open>int\<close> for t1 t2\<close> =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term ps vs (\<^term>\<open>(dvd) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>dvd \<^Type>\<open>int\<close> for t1 t2\<close> =
       (case try HOLogic.dest_number t1 of
         SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
       | NONE => error "num_of_term: unsupported dvd")
-  | fm_of_term ps vs (\<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.conj for t1 t2\<close> =
       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.disj for t1 t2\<close> =
       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.implies for t1 t2\<close> =
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (\<^term>\<open>HOL.Not\<close> $ t') =
+  | fm_of_term ps vs \<^Const_>\<open>HOL.Not for t'\<close> =
       @{code Not} (fm_of_term ps vs t')
-  | fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
+  | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       let
         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
       in @{code E} (fm_of_term ps vs' p) end
-  | fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
+  | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       let
         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
@@ -2444,44 +2444,44 @@
       let
         val q = @{code integer_of_nat} n
       in fst (the (find_first (fn (_, m) => q = m) vs)) end
-  | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: int \<Rightarrow> int\<close> $ term_of_num vs t'
-  | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
-      term_of_num vs (@{code C} i) $ term_of_num vs t2
+  | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>int\<close> for \<open>term_of_num vs t'\<close>\<close>
+  | term_of_num vs (@{code Add} (t1, t2)) =
+      \<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Sub} (t1, t2)) =
+      \<^Const>\<open>minus \<^Type>\<open>int\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Mul} (i, t2)) =
+      \<^Const>\<open>times \<^Type>\<open>int\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
   | term_of_num vs (@{code CN} (n, i, t)) =
       term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
-fun term_of_fm ps vs @{code T} = \<^term>\<open>True\<close>
-  | term_of_fm ps vs @{code F} = \<^term>\<open>False\<close>
+fun term_of_fm ps vs @{code T} = \<^Const>\<open>True\<close>
+  | term_of_fm ps vs @{code F} = \<^Const>\<open>False\<close>
   | term_of_fm ps vs (@{code Lt} t) =
-      \<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+      \<^Const>\<open>less \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
   | term_of_fm ps vs (@{code Le} t) =
-      \<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+      \<^Const>\<open>less_eq \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
   | term_of_fm ps vs (@{code Gt} t) =
-      \<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t
+      \<^Const>\<open>less \<^Type>\<open>int\<close> for \<^term>\<open>0::int\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm ps vs (@{code Ge} t) =
-      \<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t
+      \<^Const>\<open>less_eq \<^Type>\<open>int\<close> for \<^term>\<open>0::int\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm ps vs (@{code Eq} t) =
-      \<^term>\<open>(=) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+      \<^Const>\<open>HOL.eq \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
   | term_of_fm ps vs (@{code NEq} t) =
       term_of_fm ps vs (@{code Not} (@{code Eq} t))
   | term_of_fm ps vs (@{code Dvd} (i, t)) =
-      \<^term>\<open>(dvd) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs (@{code C} i) $ term_of_num vs t
+      \<^Const>\<open>dvd \<^Type>\<open>int\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm ps vs (@{code NDvd} (i, t)) =
       term_of_fm ps vs (@{code Not} (@{code Dvd} (i, t)))
   | term_of_fm ps vs (@{code Not} t') =
-      HOLogic.Not $ term_of_fm ps vs t'
+      \<^Const>\<open>HOL.Not for \<open>term_of_fm ps vs t'\<close>\<close>
   | term_of_fm ps vs (@{code And} (t1, t2)) =
-      HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+      \<^Const>\<open>HOL.conj for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
   | term_of_fm ps vs (@{code Or} (t1, t2)) =
-      HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+      \<^Const>\<open>HOL.disj for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
   | term_of_fm ps vs (@{code Imp} (t1, t2)) =
-      HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+      \<^Const>\<open>HOL.implies for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
   | term_of_fm ps vs (@{code Iff} (t1, t2)) =
-      \<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+      \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
   | term_of_fm ps vs (@{code Closed} n) =
       let
         val q = @{code integer_of_nat} n
@@ -2491,12 +2491,12 @@
 fun term_bools acc t =
   let
     val is_op =
-      member (=) [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>, \<^term>\<open>HOL.implies\<close>,
-      \<^term>\<open>(=) :: bool \<Rightarrow> _\<close>,
-      \<^term>\<open>(=) :: int \<Rightarrow> _\<close>, \<^term>\<open>(<) :: int \<Rightarrow> _\<close>,
-      \<^term>\<open>(\<le>) :: int \<Rightarrow> _\<close>, \<^term>\<open>HOL.Not\<close>, \<^term>\<open>All :: (int \<Rightarrow> _) \<Rightarrow> _\<close>,
-      \<^term>\<open>Ex :: (int \<Rightarrow> _) \<Rightarrow> _\<close>, \<^term>\<open>True\<close>, \<^term>\<open>False\<close>]
-    fun is_ty t = not (fastype_of t = HOLogic.boolT)
+      member (=) [\<^Const>\<open>HOL.conj\<close>, \<^Const>\<open>HOL.disj\<close>, \<^Const>\<open>HOL.implies\<close>,
+      \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close>,
+      \<^Const>\<open>HOL.eq \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>int\<close>\<close>,
+      \<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>HOL.Not\<close>, \<^Const>\<open>All \<^Type>\<open>int\<close>\<close>,
+      \<^Const>\<open>Ex \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>True\<close>, \<^Const>\<open>False\<close>]
+    fun is_ty t = not (fastype_of t = \<^Type>\<open>bool\<close>)
   in
     (case t of
       (l as f $ a) $ b =>
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -719,10 +719,10 @@
       val [lt, le] = map (Morphism.term phi) [\<^term>\<open>(\<sqsubset>)\<close>, \<^term>\<open>(\<sqsubseteq>)\<close>]
       fun h x t =
         case Thm.term_of t of
-          Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z =>
+          \<^Const_>\<open>HOL.eq _ for y z\<close> =>
             if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq
             else Ferrante_Rackoff_Data.Nox
-       | \<^term>\<open>Not\<close>$(Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z) =>
+       | \<^Const_>\<open>Not for \<^Const>\<open>HOL.eq _ for y z\<close>\<close> =>
             if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq
             else Ferrante_Rackoff_Data.Nox
        | b$y$z => if Term.could_unify (b, lt) then
@@ -901,27 +901,27 @@
 
 fun dest_frac ct =
   case Thm.term_of ct of
-    Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b=>
+    \<^Const_>\<open>Rings.divide _ for a b\<close> =>
       Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
-  | Const(\<^const_name>\<open>inverse\<close>, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
+  | \<^Const_>\<open>inverse _ for a\<close> => Rat.make(1, HOLogic.dest_number a |> snd)
   | t => Rat.of_int (snd (HOLogic.dest_number t))
 
 fun whatis x ct = case Thm.term_of ct of
-  Const(\<^const_name>\<open>Groups.plus\<close>, _)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$_$y)$_ =>
+  \<^Const_>\<open>plus _ for \<^Const_>\<open>times _ for _ y\<close> _\<close> =>
      if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
      else ("Nox",[])
-| Const(\<^const_name>\<open>Groups.plus\<close>, _)$y$_ =>
+| \<^Const_>\<open>plus _ for y _\<close> =>
      if y aconv Thm.term_of x then ("x+t",[Thm.dest_arg ct])
      else ("Nox",[])
-| Const(\<^const_name>\<open>Groups.times\<close>, _)$_$y =>
+| \<^Const_>\<open>times _ for _ y\<close> =>
      if y aconv Thm.term_of x then ("c*x",[Thm.dest_arg1 ct])
      else ("Nox",[])
 | t => if t aconv Thm.term_of x then ("x",[]) else ("Nox",[]);
 
 fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
-| xnormalize_conv ctxt (vs as (x::_)) ct =
+  | xnormalize_conv ctxt (vs as (x::_)) ct =
    case Thm.term_of ct of
-   Const(\<^const_name>\<open>Orderings.less\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+   \<^Const_>\<open>less _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
     (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -964,14 +964,14 @@
     | _ => Thm.reflexive ct)
 
 
-|  Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+|  \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
         val T = Thm.typ_of_cterm x
         val cT = Thm.ctyp_of_cterm x
         val cr = dest_frac c
-        val clt = Thm.cterm_of ctxt (Const (\<^const_name>\<open>ord_class.less\<close>, T --> T --> \<^typ>\<open>bool\<close>))
+        val clt = Thm.cterm_of ctxt \<^Const>\<open>less T\<close>
         val cz = Thm.dest_arg ct
         val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
@@ -996,7 +996,7 @@
         val T = Thm.typ_of_cterm x
         val cT = Thm.ctyp_of_cterm x
         val cr = dest_frac c
-        val clt = Thm.cterm_of ctxt (Const (\<^const_name>\<open>ord_class.less\<close>, T --> T --> \<^typ>\<open>bool\<close>))
+        val clt = Thm.cterm_of ctxt \<^Const>\<open>less T\<close>
         val cz = Thm.dest_arg ct
         val neg = cr < @0
         val cthp = Simplifier.rewrite ctxt
@@ -1010,7 +1010,7 @@
       in rth end
     | _ => Thm.reflexive ct)
 
-|  Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+|  \<^Const_>\<open>HOL.eq _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -1056,7 +1056,7 @@
   val ss = simpset_of \<^context>
 in
 fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of
-  Const(\<^const_name>\<open>Orderings.less\<close>,_)$a$b =>
+  \<^Const_>\<open>less _ for a b\<close> =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = Thm.ctyp_of_cterm ca
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -1065,7 +1065,7 @@
               (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$a$b =>
+| \<^Const_>\<open>less_eq _ for a b\<close> =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = Thm.ctyp_of_cterm ca
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -1075,7 +1075,7 @@
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 
-| Const(\<^const_name>\<open>HOL.eq\<close>,_)$a$b =>
+| \<^Const_>\<open>HOL.eq _ for a b\<close> =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = Thm.ctyp_of_cterm ca
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -1084,7 +1084,7 @@
               (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| \<^term>\<open>Not\<close> $(Const(\<^const_name>\<open>HOL.eq\<close>,_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for a b\<close>\<close> => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
 | _ => Thm.reflexive ct
 end;
 
@@ -1092,17 +1092,17 @@
  let
   fun h x t =
    case Thm.term_of t of
-     Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z =>
+     \<^Const_>\<open>HOL.eq _ for y z\<close> =>
       if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq
       else Ferrante_Rackoff_Data.Nox
-   | \<^term>\<open>Not\<close>$(Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z) =>
+   | \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for y z\<close>\<close> =>
       if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq
       else Ferrante_Rackoff_Data.Nox
-   | Const(\<^const_name>\<open>Orderings.less\<close>,_)$y$z =>
+   | \<^Const_>\<open>less _ for y z\<close> =>
        if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Lt
        else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Gt
        else Ferrante_Rackoff_Data.Nox
-   | Const (\<^const_name>\<open>Orderings.less_eq\<close>,_)$y$z =>
+   | \<^Const_>\<open>less_eq _ for y z\<close> =>
        if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Le
        else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Ge
        else Ferrante_Rackoff_Data.Nox
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -2458,15 +2458,15 @@
 fun num_of_term vs (Free vT) = mk_Bound (find_index (fn vT' => vT = vT') vs)
   | num_of_term vs \<^term>\<open>real_of_int (0::int)\<close> = mk_C 0
   | num_of_term vs \<^term>\<open>real_of_int (1::int)\<close> = mk_C 1
-  | num_of_term vs \<^term>\<open>0::real\<close> = mk_C 0
-  | num_of_term vs \<^term>\<open>1::real\<close> = mk_C 1
+  | num_of_term vs \<^Const_>\<open>zero_class.zero \<^Type>\<open>real\<close>\<close> = mk_C 0
+  | num_of_term vs \<^Const_>\<open>one_class.one \<^Type>\<open>real\<close>\<close> = mk_C 1
   | num_of_term vs (Bound i) = mk_Bound i
-  | num_of_term vs (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ t') = @{code Neg} (num_of_term vs t')
-  | num_of_term vs (\<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+  | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> =
      @{code Add} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> =
      @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) = (case num_of_term vs t1
+  | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> = (case num_of_term vs t1
      of @{code C} i => @{code Mul} (i, num_of_term vs t2)
       | _ => error "num_of_term: unsupported multiplication")
   | num_of_term vs (\<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $ t') =
@@ -2476,57 +2476,49 @@
      (mk_C (snd (HOLogic.dest_number t'))
        handle TERM _ => error ("num_of_term: unknown term"));
 
-fun fm_of_term vs \<^term>\<open>True\<close> = @{code T}
-  | fm_of_term vs \<^term>\<open>False\<close> = @{code F}
-  | fm_of_term vs (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term vs \<^Const_>\<open>True\<close> = @{code T}
+  | fm_of_term vs \<^Const_>\<open>False\<close> = @{code F}
+  | fm_of_term vs \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.Not\<close> $ t') = @{code Not} (fm_of_term vs t')
-  | fm_of_term vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
-      @{code E} (fm_of_term (("", dummyT) :: vs) p)
-  | fm_of_term vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
-      @{code A} (fm_of_term (("", dummyT) ::  vs) p)
+  | fm_of_term vs \<^Const_>\<open>HOL.conj for t1 t2\<close> = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs \<^Const_>\<open>HOL.disj for t1 t2\<close> = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs \<^Const_>\<open>HOL.implies for t1 t2\<close> = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs \<^Const_>\<open>HOL.Not for t'\<close> = @{code Not} (fm_of_term vs t')
+  | fm_of_term vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> = @{code E} (fm_of_term (("", dummyT) :: vs) p)
+  | fm_of_term vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> = @{code A} (fm_of_term (("", dummyT) ::  vs) p)
   | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
 
 fun term_of_num vs (@{code C} i) = \<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $
       HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
   | term_of_num vs (@{code Bound} n) = Free (nth vs (@{code integer_of_nat} n))
-  | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ term_of_num vs t'
-  | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs (@{code C} i) $ term_of_num vs t2
+  | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>
+  | term_of_num vs (@{code Add} (t1, t2)) =
+      \<^Const>\<open>plus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Sub} (t1, t2)) =
+      \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Mul} (i, t2)) =
+      \<^Const>\<open>times \<^Type>\<open>real\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
-fun term_of_fm vs @{code T} = \<^term>\<open>True\<close>
-  | term_of_fm vs @{code F} = \<^term>\<open>False\<close>
-  | term_of_fm vs (@{code Lt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
-      term_of_num vs t $ \<^term>\<open>0::real\<close>
-  | term_of_fm vs (@{code Le} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
-      term_of_num vs t $ \<^term>\<open>0::real\<close>
-  | term_of_fm vs (@{code Gt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
-      \<^term>\<open>0::real\<close> $ term_of_num vs t
-  | term_of_fm vs (@{code Ge} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
-      \<^term>\<open>0::real\<close> $ term_of_num vs t
-  | term_of_fm vs (@{code Eq} t) = \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
-      term_of_num vs t $ \<^term>\<open>0::real\<close>
+fun term_of_fm vs @{code T} = \<^Const>\<open>True\<close>
+  | term_of_fm vs @{code F} = \<^Const>\<open>False\<close>
+  | term_of_fm vs (@{code Lt} t) = \<^Const>\<open>less \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
+  | term_of_fm vs (@{code Le} t) = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
+  | term_of_fm vs (@{code Gt} t) = \<^Const>\<open>less \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
+  | term_of_fm vs (@{code Ge} t) = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
+  | term_of_fm vs (@{code Eq} t) = \<^Const>\<open>HOL.eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
   | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code Not} (@{code Eq} t))
-  | term_of_fm vs (@{code Not} t') = HOLogic.Not $ term_of_fm vs t'
-  | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
-  | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
-  | term_of_fm vs (@{code Imp}  (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
-  | term_of_fm vs (@{code Iff} (t1, t2)) = \<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $
-      term_of_fm vs t1 $ term_of_fm vs t2;
+  | term_of_fm vs (@{code Not} t') = \<^Const>\<open>HOL.Not for \<open>term_of_fm vs t'\<close>\<close>
+  | term_of_fm vs (@{code And} (t1, t2)) = \<^Const>\<open>HOL.conj for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+  | term_of_fm vs (@{code Or} (t1, t2)) = \<^Const>\<open>HOL.disj for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+  | term_of_fm vs (@{code Imp} (t1, t2)) = \<^Const>\<open>HOL.implies for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+  | term_of_fm vs (@{code Iff} (t1, t2)) = \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
 
 in fn (ctxt, t) =>
   let
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -5581,92 +5581,92 @@
   | num_of_term vs \<^term>\<open>1::real\<close> = mk_C 1
   | num_of_term vs \<^term>\<open>- 1::real\<close> = mk_C (~ 1)
   | num_of_term vs (Bound i) = mk_Bound i
-  | num_of_term vs (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ t') = @{code Neg} (num_of_term vs t')
-  | num_of_term vs (\<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+  | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Add} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+  | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (\<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
-      (case (num_of_term vs t1)
-       of @{code C} i => @{code Mul} (i, num_of_term vs t2)
-        | _ => error "num_of_term: unsupported Multiplication")
-  | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t')) =
+  | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> =
+      (case num_of_term vs t1 of
+        @{code C} i => @{code Mul} (i, num_of_term vs t2)
+      | _ => error "num_of_term: unsupported Multiplication")
+  | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t'\<close>\<close> =
       mk_C (HOLogic.dest_numeral t')
-  | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t')) =
+  | num_of_term vs (\<^Const_>\<open>of_int \<^Type>\<open>real\<close>\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t')) =  (* FIXME !? *)
       mk_C (~ (HOLogic.dest_numeral t'))
-  | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>floor :: real \<Rightarrow> int\<close> $ t')) =
+  | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>floor \<^Type>\<open>real\<close> for t'\<close>\<close> =
       @{code Floor} (num_of_term vs t')
-  | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>ceiling :: real \<Rightarrow> int\<close> $ t')) =
+  | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>ceiling \<^Type>\<open>real\<close> for t'\<close>\<close> =
       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
-  | num_of_term vs (\<^term>\<open>numeral :: _ \<Rightarrow> real\<close> $ t') =
+  | num_of_term vs \<^Const_>\<open>numeral \<^Type>\<open>real\<close> for t'\<close> =
       mk_C (HOLogic.dest_numeral t')
-  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> real\<close> $ t') =
+  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> real\<close> $ t') =  (* FIXME !? *)
       mk_C (~ (HOLogic.dest_numeral t'))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term \<^context> t);
 
-fun fm_of_term vs \<^term>\<open>True\<close> = @{code T}
-  | fm_of_term vs \<^term>\<open>False\<close> = @{code F}
-  | fm_of_term vs (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term vs \<^Const_>\<open>True\<close> = @{code T}
+  | fm_of_term vs \<^Const_>\<open>False\<close> = @{code F}
+  | fm_of_term vs \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>real\<close> for t1 t2\<close> =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
-  | fm_of_term vs (\<^term>\<open>(rdvd)\<close> $ (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t1)) $ t2) =
+  | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t1\<close>\<close> t2\<close> =
       mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>(rdvd)\<close> $ (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t1)) $ t2) =
+  | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<open>(\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t1)\<close>\<close> t2\<close> =  (* FIXME !? *)
       mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.conj for t1 t2\<close> =
       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.disj for t1 t2\<close> =
       @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) =
+  | fm_of_term vs \<^Const_>\<open>HOL.implies for t1 t2\<close> =
       @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (\<^term>\<open>HOL.Not\<close> $ t') =
+  | fm_of_term vs \<^Const_>\<open>HOL.Not for t'\<close> =
       @{code Not} (fm_of_term vs t')
-  | fm_of_term vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
-  | fm_of_term vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
+  | fm_of_term vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
       @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
   | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
 
-fun term_of_num vs (@{code C} i) = \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $
-      HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
+fun term_of_num vs (@{code C} i) =
+      \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<open>HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)\<close>\<close>
   | term_of_num vs (@{code Bound} n) =
       let
         val m = @{code integer_of_nat} n;
       in fst (the (find_first (fn (_, q) => m = q) vs)) end
   | term_of_num vs (@{code Neg} (@{code Floor} (@{code Neg} t'))) =
-      \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>ceiling :: real \<Rightarrow> int\<close> $ term_of_num vs t')
-  | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ term_of_num vs t'
-  | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-      term_of_num vs (@{code C} i) $ term_of_num vs t2
-  | term_of_num vs (@{code Floor} t) = \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>floor :: real \<Rightarrow> int\<close> $ term_of_num vs t)
+      \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<^Const>\<open>ceiling \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>\<close>
+  | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>
+  | term_of_num vs (@{code Add} (t1, t2)) =
+      \<^Const>\<open>plus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Sub} (t1, t2)) =
+      \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Mul} (i, t2)) =
+      \<^Const>\<open>times \<^Type>\<open>real\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
+  | term_of_num vs (@{code Floor} t) = \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<^Const>\<open>floor \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close>\<close>\<close>
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
   | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
 
-fun term_of_fm vs @{code T} = \<^term>\<open>True\<close>
-  | term_of_fm vs @{code F} = \<^term>\<open>False\<close>
+fun term_of_fm vs @{code T} = \<^Const>\<open>True\<close>
+  | term_of_fm vs @{code F} = \<^Const>\<open>False\<close>
   | term_of_fm vs (@{code Lt} t) =
-      \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+      \<^Const>\<open>less \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
   | term_of_fm vs (@{code Le} t) =
-      \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+      \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
   | term_of_fm vs (@{code Gt} t) =
-      \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ \<^term>\<open>0::real\<close> $ term_of_num vs t
+      \<^Const>\<open>less \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm vs (@{code Ge} t) =
-      \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ \<^term>\<open>0::real\<close> $ term_of_num vs t
+      \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm vs (@{code Eq} t) =
-      \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+      \<^Const>\<open>HOL.eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
   | term_of_fm vs (@{code NEq} t) =
       term_of_fm vs (@{code Not} (@{code Eq} t))
   | term_of_fm vs (@{code Dvd} (i, t)) =
-      \<^term>\<open>(rdvd)\<close> $ term_of_num vs (@{code C} i) $ term_of_num vs t
+      \<^Const>\<open>rdvd for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t\<close>\<close>
   | term_of_fm vs (@{code NDvd} (i, t)) =
       term_of_fm vs (@{code Not} (@{code Dvd} (i, t)))
   | term_of_fm vs (@{code Not} t') =
@@ -5678,7 +5678,7 @@
   | term_of_fm vs (@{code Imp}  (t1, t2)) =
       HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
   | term_of_fm vs (@{code Iff} (t1, t2)) =
-      \<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ term_of_fm vs t1 $ term_of_fm vs t2;
+      \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>;
 
 in
   fn (ctxt, t) =>
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -3922,9 +3922,6 @@
 \<open>
 let
 
-fun binopT T = T --> T --> T;
-fun relT T = T --> T --> \<^typ>\<open>bool\<close>;
-
 val mk_C = @{code C} o apply2 @{code int_of_integer};
 val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
 val mk_Bound = @{code Bound} o @{code nat_of_integer};
@@ -3934,7 +3931,7 @@
 fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
   handle TERM _ => NONE;
 
-fun dest_nat (t as Const (\<^const_name>\<open>Suc\<close>, _)) = HOLogic.dest_nat t
+fun dest_nat (t as \<^Const_>\<open>Suc\<close>) = HOLogic.dest_nat t  (* FIXME !? *)
   | dest_nat t = dest_num t;
 
 fun the_index ts t =
@@ -3942,58 +3939,46 @@
     val k = find_index (fn t' => t aconv t') ts;
   in if k < 0 then raise General.Subscript else k end;
 
-fun num_of_term ps (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t) =
-      @{code poly.Neg} (num_of_term ps t)
-  | num_of_term ps (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
-      @{code poly.Add} (num_of_term ps a, num_of_term ps b)
-  | num_of_term ps (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
-      @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
-  | num_of_term ps (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
-      @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
-  | num_of_term ps (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
+fun num_of_term ps \<^Const_>\<open>uminus _ for t\<close> = @{code poly.Neg} (num_of_term ps t)
+  | num_of_term ps \<^Const_>\<open>plus _ for a b\<close> = @{code poly.Add} (num_of_term ps a, num_of_term ps b)
+  | num_of_term ps \<^Const_>\<open>minus _ for a b\<close> = @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
+  | num_of_term ps \<^Const_>\<open>times _ for a b\<close> = @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
+  | num_of_term ps \<^Const_>\<open>power _ for a n\<close> =
       @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
-  | num_of_term ps (Const (\<^const_name>\<open>Rings.divide\<close>, _) $ a $ b) =
-      mk_C (dest_num a, dest_num b)
+  | num_of_term ps \<^Const_>\<open>divide _ for a b\<close> = mk_C (dest_num a, dest_num b)
   | num_of_term ps t =
       (case try_dest_num t of
         SOME k => mk_C (k, 1)
       | NONE => mk_poly_Bound (the_index ps t));
 
-fun tm_of_term fs ps (Const(\<^const_name>\<open>Groups.uminus\<close>, _) $ t) =
-      @{code Neg} (tm_of_term fs ps t)
-  | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
-      @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
-  | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
-      @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
-  | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
-      @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
+fun tm_of_term fs ps \<^Const_>\<open>uminus _ for t\<close> = @{code Neg} (tm_of_term fs ps t)
+  | tm_of_term fs ps \<^Const_>\<open>plus _ for a b\<close> = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
+  | tm_of_term fs ps \<^Const_>\<open>minus _ for a b\<close> = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
+  | tm_of_term fs ps \<^Const_>\<open>times _ for a b\<close> = @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
   | tm_of_term fs ps t = (@{code CP} (num_of_term ps t)
       handle TERM _ => mk_Bound (the_index fs t)
         | General.Subscript => mk_Bound (the_index fs t));
 
-fun fm_of_term fs ps \<^term>\<open>True\<close> = @{code T}
-  | fm_of_term fs ps \<^term>\<open>False\<close> = @{code F}
-  | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.Not\<close>, _) $ p) =
-      @{code Not} (fm_of_term fs ps p)
-  | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ p $ q) =
-      @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
-  | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ p $ q) =
-      @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
-  | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.implies\<close>, _) $ p $ q) =
+fun fm_of_term fs ps \<^Const_>\<open>True\<close> = @{code T}
+  | fm_of_term fs ps \<^Const_>\<open>False\<close> = @{code F}
+  | fm_of_term fs ps \<^Const_>\<open>HOL.Not for p\<close> = @{code Not} (fm_of_term fs ps p)
+  | fm_of_term fs ps \<^Const_>\<open>HOL.conj for p q\<close> = @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
+  | fm_of_term fs ps \<^Const_>\<open>HOL.disj for p q\<close> = @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
+  | fm_of_term fs ps \<^Const_>\<open>HOL.implies for p q\<close> =
       @{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q)
-  | fm_of_term fs ps (\<^term>\<open>HOL.iff\<close> $ p $ q) =
+  | fm_of_term fs ps \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for p q\<close> =
       @{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q)
-  | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ p $ q) =
+  | fm_of_term fs ps \<^Const_>\<open>HOL.eq _ for p q\<close> =
       @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
-  | fm_of_term fs ps (Const (\<^const_name>\<open>Orderings.less\<close>, _) $ p $ q) =
+  | fm_of_term fs ps \<^Const_>\<open>less _ for p q\<close> =
       @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
-  | fm_of_term fs ps (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ p $ q) =
+  | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> =
       @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
-  | fm_of_term fs ps (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (abs as (_, xT, _))) =
+  | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) =
       let
         val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
       in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
-  | fm_of_term fs ps (Const (\<^const_name>\<open>All\<close>,_) $ Abs (abs as (_, xT, _))) =
+  | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) =
       let
         val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
       in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
@@ -4003,64 +3988,57 @@
       let
         val (c, d) = apply2 (@{code integer_of_int}) (a, b)
       in
-        (if d = 1 then HOLogic.mk_number T c
-        else if d = 0 then Const (\<^const_name>\<open>Groups.zero\<close>, T)
-        else
-          Const (\<^const_name>\<open>Rings.divide\<close>, binopT T) $
-            HOLogic.mk_number T c $ HOLogic.mk_number T d)
+        if d = 1 then HOLogic.mk_number T c
+        else if d = 0 then \<^Const>\<open>zero_class.zero T\<close>
+        else \<^Const>\<open>divide T for \<open>HOLogic.mk_number T c\<close> \<open>HOLogic.mk_number T d\<close>\<close>
       end
   | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
   | term_of_num T ps (@{code poly.Add} (a, b)) =
-      Const (\<^const_name>\<open>Groups.plus\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+      \<^Const>\<open>plus T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
   | term_of_num T ps (@{code poly.Mul} (a, b)) =
-      Const (\<^const_name>\<open>Groups.times\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+      \<^Const>\<open>times T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
   | term_of_num T ps (@{code poly.Sub} (a, b)) =
-      Const (\<^const_name>\<open>Groups.minus\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+      \<^Const>\<open>minus T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
   | term_of_num T ps (@{code poly.Neg} a) =
-      Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ term_of_num T ps a
+      \<^Const>\<open>uminus T for \<open>term_of_num T ps a\<close>\<close>
   | term_of_num T ps (@{code poly.Pw} (a, n)) =
-      Const (\<^const_name>\<open>Power.power\<close>, T --> \<^typ>\<open>nat\<close> --> T) $
-        term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n)
+      \<^Const>\<open>power T for \<open>term_of_num T ps a\<close> \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> (@{code integer_of_nat} n)\<close>\<close>
   | term_of_num T ps (@{code poly.CN} (c, n, p)) =
       term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
 
 fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
   | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i)
   | term_of_tm T fs ps (@{code Add} (a, b)) =
-      Const (\<^const_name>\<open>Groups.plus\<close>, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
+      \<^Const>\<open>plus T for \<open>term_of_tm T fs ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
   | term_of_tm T fs ps (@{code Mul} (a, b)) =
-      Const (\<^const_name>\<open>Groups.times\<close>, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b
+      \<^Const>\<open>times T for \<open>term_of_num T ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
   | term_of_tm T fs ps (@{code Sub} (a, b)) =
-      Const (\<^const_name>\<open>Groups.minus\<close>, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
+      \<^Const>\<open>minus T for \<open>term_of_tm T fs ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
   | term_of_tm T fs ps (@{code Neg} a) =
-      Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ term_of_tm T fs ps a
+      \<^Const>\<open>uminus T for \<open>term_of_tm T fs ps a\<close>\<close>
   | term_of_tm T fs ps (@{code CNP} (n, c, p)) =
       term_of_tm T fs ps (@{code Add} (@{code Mul} (c, @{code Bound} n), p));
 
-fun term_of_fm T fs ps @{code T} = \<^term>\<open>True\<close>
-  | term_of_fm T fs ps @{code F} = \<^term>\<open>False\<close>
-  | term_of_fm T fs ps (@{code Not} p) = \<^term>\<open>HOL.Not\<close> $ term_of_fm T fs ps p
+fun term_of_fm T fs ps @{code T} = \<^Const>\<open>True\<close>
+  | term_of_fm T fs ps @{code F} = \<^Const>\<open>False\<close>
+  | term_of_fm T fs ps (@{code Not} p) = \<^Const>\<open>HOL.Not for \<open>term_of_fm T fs ps p\<close>\<close>
   | term_of_fm T fs ps (@{code And} (p, q)) =
-      \<^term>\<open>HOL.conj\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+      \<^Const>\<open>HOL.conj for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
   | term_of_fm T fs ps (@{code Or} (p, q)) =
-      \<^term>\<open>HOL.disj\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+      \<^Const>\<open>HOL.disj for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
   | term_of_fm T fs ps (@{code Imp} (p, q)) =
-      \<^term>\<open>HOL.implies\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+      \<^Const>\<open>HOL.implies for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
   | term_of_fm T fs ps (@{code Iff} (p, q)) =
-      \<^term>\<open>HOL.iff\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+      \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
   | term_of_fm T fs ps (@{code Lt} p) =
-      Const (\<^const_name>\<open>Orderings.less\<close>, relT T) $
-        term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+      \<^Const>\<open>less T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
   | term_of_fm T fs ps (@{code Le} p) =
-      Const (\<^const_name>\<open>Orderings.less_eq\<close>, relT T) $
-        term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+      \<^Const>\<open>less_eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
   | term_of_fm T fs ps (@{code Eq} p) =
-      Const (\<^const_name>\<open>HOL.eq\<close>, relT T) $
-        term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+      \<^Const>\<open>HOL.eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
   | term_of_fm T fs ps (@{code NEq} p) =
-      \<^term>\<open>Not\<close> $
-        (Const (\<^const_name>\<open>HOL.eq\<close>, relT T) $
-          term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T))
+      \<^Const>\<open>Not for (* FIXME HOL.Not!? *)
+        \<^Const>\<open>HOL.eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>\<close>
   | term_of_fm T fs ps _ = error "term_of_fm: quantifiers";
 
 fun frpar_procedure alternative T ps fm =
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Sep 29 22:54:38 2021 +0200
@@ -619,23 +619,23 @@
 qed
 
 ML \<open>
-val term_of_nat = HOLogic.mk_number \<^typ>\<open>nat\<close> o @{code integer_of_nat};
+val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
 
-val term_of_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
 
-fun term_of_pexpr (@{code PExpr1} x) = \<^term>\<open>PExpr1\<close> $ term_of_pexpr1 x
-  | term_of_pexpr (@{code PExpr2} x) = \<^term>\<open>PExpr2\<close> $ term_of_pexpr2 x
-and term_of_pexpr1 (@{code PCnst} k) = \<^term>\<open>PCnst\<close> $ term_of_int k
-  | term_of_pexpr1 (@{code PVar} n) = \<^term>\<open>PVar\<close> $ term_of_nat n
-  | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^term>\<open>PAdd\<close> $ term_of_pexpr x $ term_of_pexpr y
-  | term_of_pexpr1 (@{code PSub} (x, y)) = \<^term>\<open>PSub\<close> $ term_of_pexpr x $ term_of_pexpr y
-  | term_of_pexpr1 (@{code PNeg} x) = \<^term>\<open>PNeg\<close> $ term_of_pexpr x
-and term_of_pexpr2 (@{code PMul} (x, y)) = \<^term>\<open>PMul\<close> $ term_of_pexpr x $ term_of_pexpr y
-  | term_of_pexpr2 (@{code PPow} (x, n)) = \<^term>\<open>PPow\<close> $ term_of_pexpr x $ term_of_nat n
+fun term_of_pexpr (@{code PExpr1} x) = \<^Const>\<open>PExpr1\<close> $ term_of_pexpr1 x
+  | term_of_pexpr (@{code PExpr2} x) = \<^Const>\<open>PExpr2\<close> $ term_of_pexpr2 x
+and term_of_pexpr1 (@{code PCnst} k) = \<^Const>\<open>PCnst\<close> $ term_of_int k
+  | term_of_pexpr1 (@{code PVar} n) = \<^Const>\<open>PVar\<close> $ term_of_nat n
+  | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^Const>\<open>PAdd\<close> $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr1 (@{code PSub} (x, y)) = \<^Const>\<open>PSub\<close> $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr1 (@{code PNeg} x) = \<^Const>\<open>PNeg\<close> $ term_of_pexpr x
+and term_of_pexpr2 (@{code PMul} (x, y)) = \<^Const>\<open>PMul\<close> $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr2 (@{code PPow} (x, n)) = \<^Const>\<open>PPow\<close> $ term_of_pexpr x $ term_of_nat n
 
 fun term_of_result (x, (y, zs)) =
   HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod
-    (term_of_pexpr y, HOLogic.mk_list \<^typ>\<open>pexpr\<close> (map term_of_pexpr zs)));
+    (term_of_pexpr y, HOLogic.mk_list \<^Type>\<open>pexpr\<close> (map term_of_pexpr zs)));
 
 local
 
@@ -680,59 +680,47 @@
 
 open Ring_Tac;
 
-fun field_struct (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ R $ _ $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ R $ _ $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ R $ _ $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ R $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Group.pow\<close>, _) $ R $ _ $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Algebra_Aux.m_div\<close>, _) $ R $ _ $ _) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ R) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ R) = SOME R
-  | field_struct (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ R $ _) = SOME R
+fun field_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Algebra_Aux.m_div _ _for R _ _\<close> = SOME R
+  | field_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
+  | field_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
+  | field_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
   | field_struct _ = NONE;
 
-fun reif_fexpr vs (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>FAdd\<close> $ reif_fexpr vs a $ reif_fexpr vs b
-  | reif_fexpr vs (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>FSub\<close> $ reif_fexpr vs a $ reif_fexpr vs b
-  | reif_fexpr vs (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>FMul\<close> $ reif_fexpr vs a $ reif_fexpr vs b
-  | reif_fexpr vs (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ _ $ a) =
-      \<^const>\<open>FNeg\<close> $ reif_fexpr vs a
-  | reif_fexpr vs (Const (\<^const_name>\<open>Group.pow\<close>, _) $ _ $ a $ n) =
-      \<^const>\<open>FPow\<close> $ reif_fexpr vs a $ n
-  | reif_fexpr vs (Const (\<^const_name>\<open>Algebra_Aux.m_div\<close>, _) $ _ $ a $ b) =
-      \<^const>\<open>FDiv\<close> $ reif_fexpr vs a $ reif_fexpr vs b
+fun reif_fexpr vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
+      \<^Const>\<open>FAdd for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+  | reif_fexpr vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
+      \<^Const>\<open>FSub for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+  | reif_fexpr vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
+      \<^Const>\<open>FMul for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+  | reif_fexpr vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
+      \<^Const>\<open>FNeg for \<open>reif_fexpr vs a\<close>\<close>
+  | reif_fexpr vs \<^Const>\<open>Group.pow _ _ _ for _ a n\<close> =
+      \<^Const>\<open>FPow for \<open>reif_fexpr vs a\<close> n\<close>
+  | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.m_div _ _ for _ a b\<close> =
+      \<^Const>\<open>FDiv for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
   | reif_fexpr vs (Free x) =
-      \<^const>\<open>FVar\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
-  | reif_fexpr vs (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ _) =
-      \<^term>\<open>FCnst 0\<close>
-  | reif_fexpr vs (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ _) =
-      \<^term>\<open>FCnst 1\<close>
-  | reif_fexpr vs (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ _ $ n) =
-      \<^const>\<open>FCnst\<close> $ n
+      \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+  | reif_fexpr vs \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>FCnst 0\<close>
+  | reif_fexpr vs \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>FCnst 1\<close>
+  | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>FCnst for n\<close>
   | reif_fexpr _ _ = error "reif_fexpr: bad expression";
 
-fun reif_fexpr' vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
-      \<^const>\<open>FAdd\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
-  | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
-      \<^const>\<open>FSub\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
-  | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
-      \<^const>\<open>FMul\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
-  | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ a) =
-      \<^const>\<open>FNeg\<close> $ reif_fexpr' vs a
-  | reif_fexpr' vs (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
-      \<^const>\<open>FPow\<close> $ reif_fexpr' vs a $ n
-  | reif_fexpr' vs (Const (\<^const_name>\<open>divide\<close>, _) $ a $ b) =
-      \<^const>\<open>FDiv\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
+fun reif_fexpr' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>FAdd for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+  | reif_fexpr' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>FSub for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+  | reif_fexpr' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>FMul for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+  | reif_fexpr' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>FNeg for \<open>reif_fexpr' vs a\<close>\<close>
+  | reif_fexpr' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>FPow for \<open>reif_fexpr' vs a\<close> n\<close>
+  | reif_fexpr' vs \<^Const_>\<open>divide _ for a b\<close> = \<^Const>\<open>FDiv for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
   | reif_fexpr' vs (Free x) =
-      \<^const>\<open>FVar\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
-  | reif_fexpr' vs (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
-      \<^term>\<open>FCnst 0\<close>
-  | reif_fexpr' vs (Const (\<^const_name>\<open>one_class.one\<close>, _)) =
-      \<^term>\<open>FCnst 1\<close>
-  | reif_fexpr' vs (Const (\<^const_name>\<open>numeral\<close>, _) $ b) =
-      \<^const>\<open>FCnst\<close> $ (@{const numeral (int)} $ b)
+      \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+  | reif_fexpr' vs \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>FCnst 0\<close>
+  | reif_fexpr' vs \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>FCnst 1\<close>
+  | reif_fexpr' vs \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>FCnst for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
   | reif_fexpr' _ _ = error "reif_fexpr: bad expression";
 
 fun eq_field_simps
@@ -861,7 +849,7 @@
     fun conv xs qs = (case strip_app qs of
         (\<^const_name>\<open>Nil\<close>, []) => inst [] [xs] nonzero_Nil
       | (\<^const_name>\<open>Cons\<close>, [p, ps]) => (case Thm.term_of ps of
-            Const (\<^const_name>\<open>Nil\<close>, _) =>
+            \<^Const_>\<open>Nil _\<close> =>
               transitive' (inst [] [xs, p] nonzero_singleton)
                 (cong1 (cong2 (args2 peval_conv') Thm.reflexive))
           | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons)
@@ -873,7 +861,7 @@
     let
       val (prems, concl) = Logic.strip_horn g;
       fun find_eq s = (case s of
-          (_ $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ t $ u)) =>
+          (_ $ \<^Const_>\<open>HOL.eq T for t u\<close>) =>
             (case (field_struct t, field_struct u) of
                (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
              | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -15,12 +15,8 @@
 
 fun reorder_bounds_tac ctxt prems i =
   let
-    fun variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                           (Const (\<^const_name>\<open>Set.member\<close>, _) $
-                            Free (name, _) $ _)) = name
-      | variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-                           (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
-                            Free (name, _) $ _)) = name
+    fun variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>Set.member _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
+      | variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
       | variable_of_bound t = raise TERM ("variable_of_bound", [t])
 
     val variable_bounds
@@ -43,18 +39,18 @@
   end
 
 fun approximate ctxt t = case fastype_of t
-   of \<^typ>\<open>bool\<close> =>
+   of \<^Type>\<open>bool\<close> =>
         Approximation_Computation.approx_bool ctxt t
-    | \<^typ>\<open>(float interval) option\<close> =>
+    | \<^typ>\<open>float interval option\<close> =>
         Approximation_Computation.approx_arith ctxt t
-    | \<^typ>\<open>(float interval) option list\<close> =>
+    | \<^typ>\<open>float interval option list\<close> =>
         Approximation_Computation.approx_form_eval ctxt t
     | _ => error ("Bad term: " ^ Syntax.string_of_term ctxt t);
 
 fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
     fun lookup_splitting (Free (name, _)) =
         (case AList.lookup (op =) splitting name
-          of SOME s => HOLogic.mk_number \<^typ>\<open>nat\<close> s
+          of SOME s => HOLogic.mk_number \<^Type>\<open>nat\<close> s
            | NONE => \<^term>\<open>0 :: nat\<close>)
       | lookup_splitting t = raise TERM ("lookup_splitting", [t])
     val vs = nth (Thm.prems_of st) (i - 1)
@@ -63,16 +59,16 @@
              |> Term.strip_comb |> snd |> List.last
              |> HOLogic.dest_list
     val p = prec
-            |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+            |> HOLogic.mk_number \<^Type>\<open>nat\<close>
             |> Thm.cterm_of ctxt
   in case taylor
   of NONE => let
        val n = vs |> length
-               |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+               |> HOLogic.mk_number \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
        val s = vs
                |> map lookup_splitting
-               |> HOLogic.mk_list \<^typ>\<open>nat\<close>
+               |> HOLogic.mk_list \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
      in
        (resolve_tac ctxt [Thm.instantiate (TVars.empty,
@@ -86,7 +82,7 @@
      then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
      else let
        val t = t
-            |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+            |> HOLogic.mk_number \<^Type>\<open>nat\<close>
             |> Thm.cterm_of ctxt
        val s = vs |> map lookup_splitting |> hd
             |> Thm.cterm_of ctxt
@@ -97,42 +93,38 @@
      end
   end
 
-fun calculated_subterms (\<^const>\<open>Trueprop\<close> $ t) = calculated_subterms t
-  | calculated_subterms (\<^const>\<open>HOL.implies\<close> $ _ $ t) = calculated_subterms t
-  | calculated_subterms (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
-  | calculated_subterms (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
-  | calculated_subterms (\<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ t1 $
-                         (\<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ t2 $ t3)) = [t1, t2, t3]
+fun calculated_subterms \<^Const_>\<open>Trueprop for t\<close> = calculated_subterms t
+  | calculated_subterms \<^Const_>\<open>implies for _ t\<close> = calculated_subterms t
+  | calculated_subterms \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+  | calculated_subterms \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+  | calculated_subterms \<^Const_>\<open>Set.member \<^Type>\<open>real\<close> for
+      t1 \<^Const_>\<open>atLeastAtMost \<^Type>\<open>real\<close> for t2 t3\<close>\<close> = [t1, t2, t3]
   | calculated_subterms t = raise TERM ("calculated_subterms", [t])
 
-fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
+fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
 
-fun dest_interpret (\<^const>\<open>interpret_floatarith\<close> $ b $ xs) = (b, xs)
+fun dest_interpret \<^Const_>\<open>interpret_floatarith for b xs\<close> = (b, xs)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
 
-fun dest_interpret_env (\<^const>\<open>interpret_form\<close> $ _ $ xs) = xs
-  | dest_interpret_env (\<^const>\<open>interpret_floatarith\<close> $ _ $ xs) = xs
+fun dest_interpret_env \<^Const_>\<open>interpret_form for _ xs\<close> = xs
+  | dest_interpret_env \<^Const_>\<open>interpret_floatarith for _ xs\<close> = xs
   | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
 
-fun dest_float (\<^const>\<open>Float\<close> $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float \<^Const_>\<open>Float for m e\<close> = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
   | dest_float t = raise TERM ("dest_float", [t])
 
 
-fun dest_ivl
-  (Const (\<^const_name>\<open>Some\<close>, _) $
-    (Const (\<^const_name>\<open>Interval\<close>, _) $ ((Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)))) =
+fun dest_ivl \<^Const_>\<open>Some _ for \<^Const_>\<open>Interval _ for \<^Const_>\<open>Pair _ _ for u l\<close>\<close>\<close> =
       SOME (dest_float u, dest_float l)
-  | dest_ivl (Const (\<^const_name>\<open>None\<close>, _)) = NONE
+  | dest_ivl \<^Const_>\<open>None _\<close> = NONE
   | dest_ivl t = raise TERM ("dest_result", [t])
 
-fun mk_approx' prec t = (\<^const>\<open>approx'\<close>
-                       $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
-                       $ t $ \<^term>\<open>[] :: (float interval) option list\<close>)
+fun mk_approx' prec t =
+  \<^Const>\<open>approx' for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t \<^Const>\<open>Nil \<^typ>\<open>float interval option\<close>\<close>\<close>
 
-fun mk_approx_form_eval prec t xs = (\<^const>\<open>approx_form_eval\<close>
-                       $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
-                       $ t $ xs)
+fun mk_approx_form_eval prec t xs =
+  \<^Const>\<open>approx_form_eval for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t xs\<close>
 
 fun float2_float10 prec round_down (m, e) = (
   let
@@ -166,21 +158,21 @@
 fun mk_result prec (SOME (l, u)) =
   (let
     fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
-                       in if e = 0 then HOLogic.mk_number \<^typ>\<open>real\<close> m
-                     else if e = 1 then \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-                                        HOLogic.mk_number \<^typ>\<open>real\<close> m $
+                       in if e = 0 then HOLogic.mk_number \<^Type>\<open>real\<close> m
+                     else if e = 1 then \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+                                        HOLogic.mk_number \<^Type>\<open>real\<close> m $
                                         \<^term>\<open>10\<close>
-                                   else \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
-                                        HOLogic.mk_number \<^typ>\<open>real\<close> m $
+                                   else \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+                                        HOLogic.mk_number \<^Type>\<open>real\<close> m $
                                         (\<^term>\<open>power 10 :: nat \<Rightarrow> real\<close> $
-                                         HOLogic.mk_number \<^typ>\<open>nat\<close> (~e)) end)
-    in \<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ mk_float10 true l $ mk_float10 false u end)
+                                         HOLogic.mk_number \<^Type>\<open>nat\<close> (~e)) end)
+    in \<^Const>\<open>atLeastAtMost \<^Type>\<open>real\<close> for \<open>mk_float10 true l\<close> \<open>mk_float10 false u\<close>\<close> end)
   | mk_result _ NONE = \<^term>\<open>UNIV :: real set\<close>
 
 fun realify t =
   let
     val t = Logic.varify_global t
-    val m = map (fn (name, _) => (name, \<^typ>\<open>real\<close>)) (Term.add_tvars t [])
+    val m = map (fn (name, _) => (name, \<^Type>\<open>real\<close>)) (Term.add_tvars t [])
     val t = Term.subst_TVars m t
   in t end
 
@@ -237,12 +229,12 @@
          |> HOLogic.dest_Trueprop
          |> dest_interpret_form
          |> (fn (data, xs) =>
-            mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
-              (map (fn _ => \<^term>\<open>None :: (float interval) option\<close>) (HOLogic.dest_list xs)))
+            mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+              (map (fn _ => \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close>) (HOLogic.dest_list xs)))
          |> approximate ctxt
          |> HOLogic.dest_list
          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
-         |> map (fn (elem, s) => \<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ elem $ mk_result prec (dest_ivl s))
+         |> map (fn (elem, s) => \<^Const>\<open>Set.member \<^Type>\<open>real\<close> for elem \<open>mk_result prec (dest_ivl s)\<close>\<close>)
          |> foldr1 HOLogic.mk_conj))
 
 fun approx_arith prec ctxt t = realify t
@@ -257,8 +249,8 @@
      |> mk_result prec
 
 fun approx prec ctxt t =
-  if type_of t = \<^typ>\<open>prop\<close> then approx_form prec ctxt t
-  else if type_of t = \<^typ>\<open>bool\<close> then approx_form prec ctxt (\<^const>\<open>Trueprop\<close> $ t)
+  if type_of t = \<^Type>\<open>prop\<close> then approx_form prec ctxt t
+  else if type_of t = \<^Type>\<open>bool\<close> then approx_form prec ctxt \<^Const>\<open>Trueprop for t\<close>
   else approx_arith prec ctxt t
 
 fun approximate_cmd modes raw_t state =
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/approximation_generator.ML
--- a/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -33,33 +33,33 @@
 
 fun real_of_man_exp m e = Real.fromManExp {man = Real.fromInt m, exp = e}
 
-fun mapprox_float (\<^term>\<open>Float\<close> $ m $ e) = real_of_man_exp (int_of_term m) (int_of_term e)
+fun mapprox_float \<^Const_>\<open>Float for m e\<close> = real_of_man_exp (int_of_term m) (int_of_term e)
   | mapprox_float t = Real.fromInt (snd (HOLogic.dest_number t))
       handle TERM _ => raise TERM ("mapprox_float", [t]);
 
 (* TODO: define using compiled terms? *)
-fun mapprox_floatarith (\<^term>\<open>Add\<close> $ a $ b) xs = mapprox_floatarith a xs + mapprox_floatarith b xs
-  | mapprox_floatarith (\<^term>\<open>Minus\<close> $ a) xs = ~ (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Mult\<close> $ a $ b) xs = mapprox_floatarith a xs * mapprox_floatarith b xs
-  | mapprox_floatarith (\<^term>\<open>Inverse\<close> $ a) xs = 1.0 / mapprox_floatarith a xs
-  | mapprox_floatarith (\<^term>\<open>Cos\<close> $ a) xs = Math.cos (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Arctan\<close> $ a) xs = Math.atan (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Abs\<close> $ a) xs = abs (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Max\<close> $ a $ b) xs =
+fun mapprox_floatarith \<^Const_>\<open>Add for a b\<close> xs = mapprox_floatarith a xs + mapprox_floatarith b xs
+  | mapprox_floatarith \<^Const_>\<open>Minus for a\<close> xs = ~ (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Mult for a b\<close> xs = mapprox_floatarith a xs * mapprox_floatarith b xs
+  | mapprox_floatarith \<^Const_>\<open>Inverse for a\<close> xs = 1.0 / mapprox_floatarith a xs
+  | mapprox_floatarith \<^Const_>\<open>Cos for a\<close> xs = Math.cos (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Arctan for a\<close> xs = Math.atan (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Abs for a\<close> xs = abs (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Max for a b\<close> xs =
       Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith (\<^term>\<open>Min\<close> $ a $ b) xs =
+  | mapprox_floatarith \<^Const_>\<open>Min for a b\<close> xs =
       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith \<^term>\<open>Pi\<close> _ = Math.pi
-  | mapprox_floatarith (\<^term>\<open>Sqrt\<close> $ a) xs = Math.sqrt (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Exp\<close> $ a) xs = Math.exp (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Powr\<close> $ a $ b) xs =
+  | mapprox_floatarith \<^Const_>\<open>Pi\<close> _ = Math.pi
+  | mapprox_floatarith \<^Const_>\<open>Sqrt for a\<close> xs = Math.sqrt (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Exp for a\<close> xs = Math.exp (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Powr for a b\<close> xs =
       Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
-  | mapprox_floatarith (\<^term>\<open>Ln\<close> $ a) xs = Math.ln (mapprox_floatarith a xs)
-  | mapprox_floatarith (\<^term>\<open>Power\<close> $ a $ n) xs =
+  | mapprox_floatarith \<^Const_>\<open>Ln for a\<close> xs = Math.ln (mapprox_floatarith a xs)
+  | mapprox_floatarith \<^Const_>\<open>Power for a n\<close> xs =
       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
-  | mapprox_floatarith (\<^term>\<open>Floor\<close> $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
-  | mapprox_floatarith (\<^term>\<open>Var\<close> $ n) xs = nth xs (nat_of_term n)
-  | mapprox_floatarith (\<^term>\<open>Num\<close> $ m) _ = mapprox_float m
+  | mapprox_floatarith \<^Const_>\<open>Floor for a\<close> xs = Real.fromInt (floor (mapprox_floatarith a xs))
+  | mapprox_floatarith \<^Const_>\<open>Var for n\<close> xs = nth xs (nat_of_term n)
+  | mapprox_floatarith \<^Const_>\<open>Num for m\<close> _ = mapprox_float m
   | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
 
 fun mapprox_atLeastAtMost eps x a b xs =
@@ -69,23 +69,20 @@
       mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
     end
 
-fun mapprox_form eps (\<^term>\<open>Bound\<close> $ x $ a $ b $ f) xs =
+fun mapprox_form eps \<^Const_>\<open>Bound for x a b f\<close> xs =
     (not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Assign\<close> $ x $ a $ f) xs =
+| mapprox_form eps \<^Const_>\<open>Assign for x a f\<close> xs =
     (Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Less\<close> $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>LessEqual\<close> $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>AtLeastAtMost\<close> $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs
-| mapprox_form eps (\<^term>\<open>Conj\<close> $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs
-| mapprox_form eps (\<^term>\<open>Disj\<close> $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Less for a b\<close> xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>LessEqual for a b\<close> xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>AtLeastAtMost for x a b\<close> xs = mapprox_atLeastAtMost eps x a b xs
+| mapprox_form eps \<^Const_>\<open>Conj for f g\<close> xs = mapprox_form eps f xs andalso mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Disj for f g\<close> xs = mapprox_form eps f xs orelse mapprox_form eps g xs
 | mapprox_form _ t _ = raise TERM ("mapprox_form", [t])
 
-fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
+fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
 
-fun optionT t = Type (\<^type_name>\<open>option\<close>, [t])
-fun mk_Some t = Const (\<^const_name>\<open>Some\<close>, t --> optionT t)
-
 fun random_float_list size xs seed =
   fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed)
 
@@ -96,7 +93,7 @@
 
 fun term_of_Float (@{code Float} (m, e)) = @{term Float} $ term_of_int m $ term_of_int e
 
-fun is_True \<^term>\<open>True\<close> = true
+fun is_True \<^Const_>\<open>True\<close> = true
   | is_True _ = false
 
 val postproc_form_eqs =
@@ -130,12 +127,12 @@
   let
     val (rs, seed') = random_float_list size xs seed
     fun mk_approx_form e ts =
-      \<^const>\<open>approx_form\<close> $
-        HOLogic.mk_number \<^typ>\<open>nat\<close> prec $
+      \<^Const>\<open>approx_form\<close> $
+        HOLogic.mk_number \<^Type>\<open>nat\<close> prec $
         e $
-        (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
-          (map (fn t => mk_Some \<^typ>\<open>float interval\<close> $ (\<^term>\<open>interval_of::float\<Rightarrow>_\<close> $ t)) ts)) $
-        \<^term>\<open>[] :: nat list\<close>
+        (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+          (map (fn t => \<^Const>\<open>Some \<^typ>\<open>float interval\<close>\<close> $ \<^Const>\<open>interval_of \<^Type>\<open>float\<close> for t\<close>) ts)) $
+        \<^Const>\<open>Nil \<^Type>\<open>nat\<close>\<close>
   in
     (if
       mapprox_form eps e (map (real_of_Float o fst) rs)
@@ -150,7 +147,7 @@
         val ts' = map
           (AList.lookup op = (map dest_Free xs ~~ ts)
             #> the_default Term.dummy
-            #> curry op $ \<^term>\<open>real_of_float::float\<Rightarrow>_\<close>
+            #> curry op $ \<^Const>\<open>real_of_float\<close>
             #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
           frees
       in
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -26,7 +26,7 @@
     val np = length ps
     val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (List.foldr HOLogic.mk_imp c rhs, np) ps
-    val (vs, _) = List.partition (fn t => q orelse (type_of t) = \<^typ>\<open>nat\<close>)
+    val (vs, _) = List.partition (fn t => q orelse (type_of t) = \<^Type>\<open>nat\<close>)
       (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
     val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
@@ -84,7 +84,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) =
       (case Thm.prop_of pre_thm of
-        Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+        \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
           let
             val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1)
           in
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -63,7 +63,7 @@
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case Thm.prop_of pre_thm of
-        Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+        \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
     let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     in 
        ((pth RS iffD2) RS pre_thm,
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -33,12 +33,12 @@
              {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
 let
  fun uset (vars as (x::vs)) p = case Thm.term_of p of
-   Const(\<^const_name>\<open>HOL.conj\<close>, _)$ _ $ _ =>
+   \<^Const_>\<open>HOL.conj for _ _\<close> =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
      in (lS@rS, Drule.binop_cong_rule b lth rth) end
- |  Const(\<^const_name>\<open>HOL.disj\<close>, _)$ _ $ _ =>
+ | \<^Const_>\<open>HOL.disj for _ _\<close> =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
@@ -78,7 +78,7 @@
  fun main vs p =
   let
    val ((xn,ce),(x,fm)) = (case Thm.term_of p of
-                   Const(\<^const_name>\<open>Ex\<close>,_)$Abs(xn,xT,_) =>
+                   \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> =>
                         Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
                  | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    val cT = Thm.ctyp_of_cterm x
@@ -99,8 +99,8 @@
    in
     fun provein x S =
      case Thm.term_of S of
-        Const(\<^const_name>\<open>Orderings.bot\<close>, _) => raise CTERM ("provein : not a member!", [S])
-      | Const(\<^const_name>\<open>insert\<close>, _) $ y $_ =>
+        \<^Const_>\<open>Orderings.bot _\<close> => raise CTERM ("provein : not a member!", [S])
+      | \<^Const_>\<open>insert _ for y _\<close> =>
          let val (cy,S') = Thm.dest_binop S
          in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
          else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
@@ -123,12 +123,12 @@
 
    fun decomp_mpinf fm =
      case Thm.term_of fm of
-       Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ =>
+       \<^Const_>\<open>HOL.conj for _ _\<close> =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
                          (Thm.lambda x p) (Thm.lambda x q))
         end
-     | Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ =>
+     | \<^Const_>\<open>HOL.disj for _ _\<close> =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
                          (Thm.lambda x p) (Thm.lambda x q))
@@ -176,19 +176,17 @@
  let
   fun h bounds tm =
    (case Thm.term_of tm of
-     Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
-       if domain_type T = HOLogic.boolT then find_args bounds tm
-       else Thm.dest_fun2 tm
-   | Const (\<^const_name>\<open>Not\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
-   | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
-   | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
-   | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
-   | Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => find_args bounds tm
-   | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => find_args bounds tm
-   | Const (\<^const_name>\<open>Pure.all\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
+     \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
+   | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+   | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+   | \<^Const_>\<open>conj for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>disj for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>implies for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
+   | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+   | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
    | _ => Thm.dest_fun2 tm)
   and find_args bounds tm =
            (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -15,8 +15,8 @@
   let
     fun h acc ct =
       (case Thm.term_of ct of
-        Const (\<^const_name>\<open>Orderings.bot\<close>, _) => acc
-      | Const (\<^const_name>\<open>insert\<close>, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
+        \<^Const_>\<open>bot _\<close> => acc
+      | \<^Const_>\<open>insert _ for _ _\<close> => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
   in h [] end;
 
 fun prove_finite cT u =
@@ -34,7 +34,7 @@
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
   (case Thm.term_of ep of
-    Const (\<^const_name>\<open>Ex\<close>, _) $ _ =>
+    \<^Const_>\<open>Ex _ for _\<close> =>
       let
         val p = Thm.dest_arg ep
         val ths =
@@ -53,10 +53,10 @@
 
         val qe =
           (case (Thm.term_of L, Thm.term_of U) of
-            (Const (\<^const_name>\<open>Orderings.bot\<close>, _),_) =>
+            (\<^Const_>\<open>bot _\<close>, _) =>
               let val (neU, fU) = proveneF U
               in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
-          | (_, Const (\<^const_name>\<open>Orderings.bot\<close>, _)) =>
+          | (_, \<^Const_>\<open>bot _\<close>) =>
               let val (neL,fL) = proveneF L
               in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
           | _ =>
@@ -71,13 +71,13 @@
   let
     fun h acc ct =
       (case Thm.term_of ct of
-        \<^term>\<open>HOL.conj\<close> $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+        \<^Const>\<open>HOL.conj for _ _\<close> => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
       | _ => ct :: acc)
   in h [] end;
 
 fun conjuncts ct =
   (case Thm.term_of ct of
-    \<^term>\<open>HOL.conj\<close> $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
+    \<^Const>\<open>HOL.conj for _ _\<close> => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
   | _ => [ct]);
 
 fun fold1 f = foldr1 (uncurry f);  (* FIXME !? *)
@@ -89,12 +89,12 @@
   let
     fun h acc th =
       (case Thm.prop_of th of
-        \<^term>\<open>Trueprop\<close> $ (\<^term>\<open>HOL.conj\<close> $ p $ q) =>
+        \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.conj for p q\<close>\<close> =>
           h (h acc (th RS conjunct2)) (th RS conjunct1)
-      | \<^term>\<open>Trueprop\<close> $ p => (p, th) :: acc)
+      | \<^Const_>\<open>Trueprop for p\<close> => (p, th) :: acc)
   in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
-fun is_conj (\<^term>\<open>HOL.conj\<close>$_$_) = true
+fun is_conj \<^Const_>\<open>HOL.conj for _ _\<close> = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs =
@@ -122,7 +122,7 @@
 
 fun is_eqx x eq =
   (case Thm.term_of eq of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ l $ r =>
+    \<^Const_>\<open>HOL.eq _ for l r\<close> =>
       l aconv Thm.term_of x orelse r aconv Thm.term_of x
   | _ => false);
 
@@ -130,7 +130,7 @@
 
 fun proc ctxt ct =
   (case Thm.term_of ct of
-    Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, _, _) =>
+    \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
       let
         val e = Thm.dest_fun ct
         val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -197,19 +197,17 @@
   let
     fun h bounds tm =
       (case Thm.term_of tm of
-        Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
-          if domain_type T = HOLogic.boolT then find_args bounds tm
-          else Thm.dest_fun2 tm
-      | Const (\<^const_name>\<open>Not\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
-      | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-      | Const (\<^const_name>\<open>Pure.all\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-      | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
-      | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
-      | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
-      | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
-      | Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => find_args bounds tm
-      | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => find_args bounds tm
-      | Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
+        \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
+      | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+      | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+      | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+      | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
+      | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
       | _ => Thm.dest_fun2 tm)
     and find_args bounds tm =
       (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
diff -r dc73f9e6476b -r e80c4cde6064 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Sep 29 22:54:38 2021 +0200
@@ -105,7 +105,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) =
       case Thm.prop_of pre_thm of
-        Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+        \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
     let
       val pth = mirfr_oracle (ctxt, Envir.eta_long [] t1)
     in