# HG changeset patch
# User wenzelm
# Date 1632859821 -7200
# Node ID 79ac28db185cf9466512a31ffdd04cecbe7f945f
# Parent  9ea507f63bcb62633892592a08a42b39064fcf73
clarified antiquotations;

diff -r 9ea507f63bcb -r 79ac28db185c src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 28 22:10:21 2021 +0200
@@ -182,8 +182,7 @@
 
 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
 
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close>
-                         $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
   | has_lonely_bool_var _ = false
 
 val syntactic_sorts =
diff -r 9ea507f63bcb -r 79ac28db185c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 28 22:10:21 2021 +0200
@@ -331,16 +331,16 @@
   else
     s
 
-fun s_conj (t1, \<^const>\<open>True\<close>) = t1
-  | s_conj (\<^const>\<open>True\<close>, t2) = t2
+fun s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+  | s_conj (\<^Const_>\<open>True\<close>, t2) = t2
   | s_conj (t1, t2) =
-    if t1 = \<^const>\<open>False\<close> orelse t2 = \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
+    if t1 = \<^Const>\<open>False\<close> orelse t2 = \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
     else HOLogic.mk_conj (t1, t2)
 
-fun s_disj (t1, \<^const>\<open>False\<close>) = t1
-  | s_disj (\<^const>\<open>False\<close>, t2) = t2
+fun s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+  | s_disj (\<^Const_>\<open>False\<close>, t2) = t2
   | s_disj (t1, t2) =
-    if t1 = \<^const>\<open>True\<close> orelse t2 = \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
+    if t1 = \<^Const>\<open>True\<close> orelse t2 = \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
     else HOLogic.mk_disj (t1, t2)
 
 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -348,13 +348,13 @@
   | strip_connective _ t = [t]
 
 fun strip_any_connective (t as (t0 $ _ $ _)) =
-    if t0 = \<^const>\<open>HOL.conj\<close> orelse t0 = \<^const>\<open>HOL.disj\<close> then
+    if t0 = \<^Const>\<open>conj\<close> orelse t0 = \<^Const>\<open>disj\<close> then
       (strip_connective t0 t, t0)
     else
-      ([t], \<^const>\<open>Not\<close>)
-  | strip_any_connective t = ([t], \<^const>\<open>Not\<close>)
-val conjuncts_of = strip_connective \<^const>\<open>HOL.conj\<close>
-val disjuncts_of = strip_connective \<^const>\<open>HOL.disj\<close>
+      ([t], \<^Const>\<open>Not\<close>)
+  | strip_any_connective t = ([t], \<^Const>\<open>Not\<close>)
+val conjuncts_of = strip_connective \<^Const>\<open>conj\<close>
+val disjuncts_of = strip_connective \<^Const>\<open>disj\<close>
 
 (* When you add constants to these lists, make sure to handle them in
    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -797,8 +797,8 @@
         the (Quotient_Info.lookup_quotients thy s)
       val partial =
         case Thm.prop_of equiv_thm of
-          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
-        | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
+          \<^Const_>\<open>Trueprop for \<^Const_>\<open>equivp _ for _\<close>\<close> => false
+        | \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
         | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
                                    \relation theorem"
       val Ts' = qtyp |> dest_Type |> snd
@@ -948,7 +948,7 @@
       fold (fn (z as ((s, _), T)) => fn t' =>
                Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
            (take (length zs' - length zs) zs')
-    fun aux zs (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
+    fun aux zs \<^Const>\<open>Pure.imp for t1 t2\<close> =
         let val zs' = Term.add_vars t1 zs in
           close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
         end
@@ -957,8 +957,8 @@
 
 fun distinctness_formula T =
   all_distinct_unordered_pairs_of
-  #> map (fn (t1, t2) => \<^const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
-  #> List.foldr (s_conj o swap) \<^const>\<open>True\<close>
+  #> map (fn (t1, t2) => \<^Const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
+  #> List.foldr (s_conj o swap) \<^Const>\<open>True\<close>
 
 fun zero_const T = Const (\<^const_name>\<open>zero_class.zero\<close>, T)
 fun suc_const T = Const (\<^const_name>\<open>Suc\<close>, T --> T)
@@ -986,7 +986,7 @@
                SOME {abs_type, rep_type, Abs_name, ...} =>
                [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
              | NONE =>
-               if T = \<^typ>\<open>ind\<close> then [dest_Const \<^const>\<open>Zero_Rep\<close>, dest_Const \<^const>\<open>Suc_Rep\<close>]
+               if T = \<^typ>\<open>ind\<close> then [dest_Const \<^Const>\<open>Zero_Rep\<close>, dest_Const \<^Const>\<open>Suc_Rep\<close>]
                else [])
   | uncached_data_type_constrs _ _ = []
 
@@ -1145,8 +1145,8 @@
     if t1' aconv t2 then \<^prop>\<open>True\<close> else t1 $ t2
   | s_betapply _ (t1 as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1', t2) =
     if t1' aconv t2 then \<^term>\<open>True\<close> else t1 $ t2
-  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>True\<close> $ t1', _) = t1'
-  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>False\<close> $ _, t2) = t2
+  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>True\<close> $ t1', _) = t1'
+  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>False\<close> $ _, t2) = t2
   | s_betapply Ts (Const (\<^const_name>\<open>Let\<close>,
                           Type (_, [bound_T, Type (_, [_, body_T])]))
                    $ t12 $ Abs (s, T, t13'), t2) =
@@ -1181,18 +1181,18 @@
 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   let val dataT = body_type T in
     if s = \<^const_name>\<open>Suc\<close> then
-      Abs (Name.uu, dataT, \<^const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
+      Abs (Name.uu, dataT, \<^Const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
     else if length (data_type_constrs hol_ctxt dataT) >= 2 then
       Const (discr_for_constr x)
     else
-      Abs (Name.uu, dataT, \<^const>\<open>True\<close>)
+      Abs (Name.uu, dataT, \<^Const>\<open>True\<close>)
   end
 
 fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
   case head_of t of
     Const x' =>
-    if x = x' then \<^const>\<open>True\<close>
-    else if is_nonfree_constr ctxt x' then \<^const>\<open>False\<close>
+    if x = x' then \<^Const>\<open>True\<close>
+    else if is_nonfree_constr ctxt x' then \<^Const>\<open>False\<close>
     else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
 
@@ -1379,10 +1379,10 @@
    simplification rules (equational specifications). *)
 fun term_under_def t =
   case t of
-    \<^const>\<open>Pure.imp\<close> $ _ $ t2 => term_under_def t2
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => term_under_def t1
-  | \<^const>\<open>Trueprop\<close> $ t1 => term_under_def t1
-  | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => term_under_def t1
+    \<^Const_>\<open>Pure.imp for _ t2\<close> => term_under_def t2
+  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => term_under_def t1
+  | \<^Const_>\<open>Trueprop for t1\<close> => term_under_def t1
+  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => term_under_def t1
   | Abs (_, _, t') => term_under_def t'
   | t1 $ _ => term_under_def t1
   | _ => t
@@ -1405,9 +1405,8 @@
       | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
-        Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => (t1, t2)
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
-        (t1, t2)
+        \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => (t1, t2)
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close> => (t1, t2)
       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
     val args = strip_comb lhs |> snd
   in fold_rev aux args (SOME rhs) end
@@ -1482,13 +1481,13 @@
 
 fun lhs_of_equation t =
   case t of
-    Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => SOME t1
-  | \<^const>\<open>Pure.imp\<close> $ _ $ t2 => lhs_of_equation t2
-  | \<^const>\<open>Trueprop\<close> $ t1 => lhs_of_equation t1
-  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
-  | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => SOME t1
-  | \<^const>\<open>HOL.implies\<close> $ _ $ t2 => lhs_of_equation t2
+    \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => SOME t1
+  | \<^Const_>\<open>Pure.imp for _ t2\<close> => lhs_of_equation t2
+  | \<^Const_>\<open>Trueprop for t1\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>All _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+  | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => SOME t1
+  | \<^Const_>\<open>implies for _ t2\<close> => lhs_of_equation t2
   | _ => NONE
 
 fun is_constr_pattern _ (Bound _) = true
@@ -1598,19 +1597,19 @@
                                    (incr_boundvars 1 func_t, x),
                   discriminate_value hol_ctxt x (Bound 0)))
       |> AList.group (op aconv)
-      |> map (apsnd (List.foldl s_disj \<^const>\<open>False\<close>))
+      |> map (apsnd (List.foldl s_disj \<^Const>\<open>False\<close>))
       |> sort (int_ord o apply2 (size_of_term o snd))
       |> rev
   in
     if res_T = bool_T then
-      if forall (member (op =) [\<^const>\<open>False\<close>, \<^const>\<open>True\<close>] o fst) cases then
+      if forall (member (op =) [\<^Const>\<open>False\<close>, \<^Const>\<open>True\<close>] o fst) cases then
         case cases of
           [(body_t, _)] => body_t
-        | [_, (\<^const>\<open>True\<close>, head_t2)] => head_t2
-        | [_, (\<^const>\<open>False\<close>, head_t2)] => \<^const>\<open>Not\<close> $ head_t2
+        | [_, (\<^Const>\<open>True\<close>, head_t2)] => head_t2
+        | [_, (\<^Const>\<open>False\<close>, head_t2)] => \<^Const>\<open>Not for head_t2\<close>
         | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
       else
-        \<^const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
+        \<^Const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
     else
       fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
   end
@@ -1895,13 +1894,12 @@
   in
     Logic.list_implies (prems,
         case concl of
-          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
-                               $ t1 $ t2) =>
-          \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
-        | \<^const>\<open>Trueprop\<close> $ t' =>
-          \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (t', \<^const>\<open>True\<close>)
-        | Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
-          \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
+          \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for t1 t2\<close>\<close> =>
+          \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
+        | \<^Const_>\<open>Trueprop for t'\<close> =>
+          \<^Const>\<open>Trueprop for \<open>HOLogic.mk_eq (t', \<^Const>\<open>True\<close>)\<close>\<close>
+        | \<^Const_>\<open>Pure.eq T for t1 t2\<close> =>
+          \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
         | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
                          quote (Syntax.string_of_term ctxt t));
                 raise SAME ()))
@@ -1951,7 +1949,7 @@
   end
 
 fun ground_theorem_table thy =
-  fold ((fn \<^const>\<open>Trueprop\<close> $ t1 =>
+  fold ((fn \<^Const_>\<open>Trueprop for t1\<close> =>
             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
           | _ => I) o Thm.prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
 
@@ -2016,13 +2014,13 @@
   in
     [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
      Logic.list_implies
-         ([\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
-           \<^const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
+         ([\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
+           \<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
            equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
            Logic.mk_equals (normal_x, normal_y)),
      Logic.list_implies
-         ([HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
-           HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
+         ([HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
+           HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
     |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
   end
@@ -2031,8 +2029,8 @@
   let
     val xs = data_type_constrs hol_ctxt T
     val pred_T = T --> bool_T
-    val iter_T = \<^typ>\<open>bisim_iterator\<close>
-    val bisim_max = \<^const>\<open>bisim_iterator_max\<close>
+    val iter_T = \<^Type>\<open>bisim_iterator\<close>
+    val bisim_max = \<^Const>\<open>bisim_iterator_max\<close>
     val n_var = Var (("n", 0), iter_T)
     val n_var_minus_1 =
       Const (\<^const_name>\<open>safe_The\<close>, (iter_T --> bool_T) --> iter_T)
@@ -2214,8 +2212,8 @@
           fun repair_rec j (Const (\<^const_name>\<open>Ex\<close>, T1) $ Abs (s2, T2, t2')) =
               Const (\<^const_name>\<open>Ex\<close>, T1)
               $ Abs (s2, T2, repair_rec (j + 1) t2')
-            | repair_rec j (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
-              \<^const>\<open>HOL.conj\<close> $ repair_rec j t1 $ repair_rec j t2
+            | repair_rec j \<^Const_>\<open>conj for t1 t2\<close> =
+              \<^Const>\<open>conj for \<open>repair_rec j t1\<close> \<open>repair_rec j t2\<close>\<close>
             | repair_rec j t =
               let val (head, args) = strip_comb t in
                 if head = Bound j then
@@ -2227,9 +2225,9 @@
           val (nonrecs, recs) =
             List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
                            (disjuncts_of body)
-          val base_body = nonrecs |> List.foldl s_disj \<^const>\<open>False\<close>
+          val base_body = nonrecs |> List.foldl s_disj \<^Const>\<open>False\<close>
           val step_body = recs |> map (repair_rec j)
-                               |> List.foldl s_disj \<^const>\<open>False\<close>
+                               |> List.foldl s_disj \<^Const>\<open>False\<close>
         in
           (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
            |> ap_n_split (length arg_Ts) tuple_T bool_T,
@@ -2241,11 +2239,7 @@
   in aux end
 
 fun predicatify T t =
-  let val set_T = HOLogic.mk_setT T in
-    Abs (Name.uu, T,
-         Const (\<^const_name>\<open>Set.member\<close>, T --> set_T --> bool_T)
-         $ Bound 0 $ incr_boundvars 1 t)
-  end
+  Abs (Name.uu, T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> \<open>incr_boundvars 1 t\<close>\<close>)
 
 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
   let
@@ -2365,7 +2359,7 @@
                       [inductive_pred_axiom hol_ctxt x]
                     else case def_of_const thy def_tables x of
                       SOME def =>
-                      \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
+                      \<^Const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
                       |> equationalize_term ctxt "" |> the |> single
                     | NONE => [])
            | psimps => psimps)
@@ -2373,7 +2367,7 @@
 
 fun is_equational_fun_surely_complete hol_ctxt x =
   case equational_fun_axioms hol_ctxt x of
-    [\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
+    [\<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 _\<close>\<close>] =>
     strip_comb t1 |> snd |> forall is_Var
   | _ => false
 
diff -r 9ea507f63bcb -r 79ac28db185c src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 28 22:10:21 2021 +0200
@@ -333,8 +333,8 @@
         else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
   in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
 
-fun truth_const_sort_key \<^const>\<open>True\<close> = "0"
-  | truth_const_sort_key \<^const>\<open>False\<close> = "2"
+fun truth_const_sort_key \<^Const_>\<open>True\<close> = "0"
+  | truth_const_sort_key \<^Const_>\<open>False\<close> = "2"
   | truth_const_sort_key _ = "1"
 
 fun mk_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) ts =
@@ -411,14 +411,14 @@
               empty_const
           | aux ((t1, t2) :: zs) =
             aux zs
-            |> t2 <> \<^const>\<open>False\<close>
+            |> t2 <> \<^Const>\<open>False\<close>
                ? curry (op $)
                        (insert_const
-                        $ (t1 |> t2 <> \<^const>\<open>True\<close>
+                        $ (t1 |> t2 <> \<^Const>\<open>True\<close>
                                  ? curry (op $)
                                          (Const (maybe_name, T --> T))))
       in
-        if forall (fn (_, t) => t <> \<^const>\<open>True\<close> andalso t <> \<^const>\<open>False\<close>)
+        if forall (fn (_, t) => t <> \<^Const>\<open>True\<close> andalso t <> \<^Const>\<open>False\<close>)
                   tps then
           Const (unknown, set_T)
         else
@@ -516,7 +516,7 @@
       | term_for_atom seen \<^typ>\<open>prop\<close> _ j k =
         HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
       | term_for_atom _ \<^typ>\<open>bool\<close> _ j _ =
-        if j = 0 then \<^const>\<open>False\<close> else \<^const>\<open>True\<close>
+        if j = 0 then \<^Const>\<open>False\<close> else \<^Const>\<open>True\<close>
       | term_for_atom seen T _ j k =
         if T = nat_T then
           HOLogic.mk_number nat_T j
@@ -524,7 +524,7 @@
           HOLogic.mk_number int_T (int_for_atom (k, 0) j)
         else if is_fp_iterator_type T then
           HOLogic.mk_number nat_T (k - j - 1)
-        else if T = \<^typ>\<open>bisim_iterator\<close> then
+        else if T = \<^Type>\<open>bisim_iterator\<close> then
           HOLogic.mk_number nat_T j
         else case data_type_spec data_types T of
           NONE => nth_atom thy atomss pool T j
diff -r 9ea507f63bcb -r 79ac28db185c src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 28 22:10:21 2021 +0200
@@ -829,10 +829,10 @@
                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
                            " : _?");
        case t of
-         \<^const>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
+         \<^Const_>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
        | Const (\<^const_name>\<open>None\<close>, T) =>
          (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
-       | \<^const>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
+       | \<^Const_>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
        | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ Bound 0 $ t2 =>
          (* hack to exploit symmetry of equality when typing "insert" *)
          (if t2 = Bound 0 then do_term \<^term>\<open>True\<close>
@@ -850,9 +850,9 @@
             | \<^const_name>\<open>Ex\<close> =>
               let val set_T = domain_type T in
                 do_term (Abs (Name.uu, set_T,
-                              \<^const>\<open>Not\<close> $ (HOLogic.mk_eq
+                              \<^Const>\<open>Not\<close> $ (HOLogic.mk_eq
                                   (Abs (Name.uu, domain_type set_T,
-                                        \<^const>\<open>False\<close>),
+                                        \<^Const>\<open>False\<close>),
                                    Bound 0)))) accum
               end
             | \<^const_name>\<open>HOL.eq\<close> => do_equals T accum
@@ -971,12 +971,11 @@
                         val (M', accum) =
                           do_term t' (accum |>> push_bound (V x) T M)
                       in (MFun (M, V x, M'), accum |>> pop_bound) end))
-         | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec t1 \<^const>\<open>False\<close> accum
-         | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec t1 t2 accum
-         | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec t1 t2 accum
-         | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec t1 t2 accum
-         | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
-           do_term (betapply (t2, t1)) accum
+         | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec t1 \<^Const>\<open>False\<close> accum
+         | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec t1 t2 accum
+         | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec t1 t2 accum
+         | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec t1 t2 accum
+         | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_term (betapply (t2, t1)) accum
          | t1 $ t2 =>
            let
              fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
@@ -1060,7 +1059,7 @@
           Const (s as \<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) =>
           do_quantifier s T1 t1
         | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
-        | \<^const>\<open>Trueprop\<close> $ t1 => do_formula sn t1 accum
+        | \<^Const_>\<open>Trueprop for t1\<close> => do_formula sn t1 accum
         | Const (s as \<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) =>
           do_quantifier s T1 t1
         | Const (s as \<^const_name>\<open>Ex\<close>, T0) $ (t1 as Abs (_, T1, t1')) =>
@@ -1068,19 +1067,17 @@
              Plus => do_quantifier s T1 t1'
            | Minus =>
              (* FIXME: Needed? *)
-             do_term (\<^const>\<open>Not\<close>
+             do_term (\<^Const>\<open>Not\<close>
                       $ (HOLogic.eq_const (domain_type T0) $ t1
-                         $ Abs (Name.uu, T1, \<^const>\<open>False\<close>))) accum)
-        | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
-        | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
-          do_formula sn (betapply (t2, t1)) accum
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          do_connect meta_conj_spec false t1 t2 accum
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
-        | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec true t1 \<^const>\<open>False\<close> accum
-        | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
-        | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
-        | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
+                         $ Abs (Name.uu, T1, \<^Const>\<open>False\<close>))) accum)
+        | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => do_equals t1 t2
+        | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_formula sn (betapply (t2, t1)) accum
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => do_connect meta_conj_spec false t1 t2 accum
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_connect meta_imp_spec true t1 t2 accum
+        | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec true t1 \<^Const>\<open>False\<close> accum
+        | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec false t1 t2 accum
+        | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec false t1 t2 accum
+        | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec true t1 t2 accum
         | _ => do_term t accum
       end
       |> tap (fn (gamma, _) =>
@@ -1122,18 +1119,15 @@
       and do_implies t1 t2 = do_term t1 #> do_formula t2
       and do_formula t accum =
         case t of
-          Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
-        | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1 accum
-        | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 =>
-          consider_general_equals mdata true t1 t2 accum
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_implies t1 t2 accum
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          fold (do_formula) [t1, t2] accum
-        | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
-        | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 =>
-          consider_general_equals mdata true t1 t2 accum
-        | \<^const>\<open>conj\<close> $ t1 $ t2 => fold (do_formula) [t1, t2] accum
-        | \<^const>\<open>implies\<close> $ t1 $ t2 => do_implies t1 t2 accum
+          \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+        | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1 accum
+        | \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_implies t1 t2 accum
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+        | \<^Const_>\<open>All _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+        | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+        | \<^Const_>\<open>conj for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+        | \<^Const_>\<open>implies for t1 t2\<close> => do_implies t1 t2 accum
         | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                            \do_formula", [t])
     in do_formula t end
diff -r 9ea507f63bcb -r 79ac28db185c src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 28 22:10:21 2021 +0200
@@ -36,15 +36,12 @@
 
 val may_use_binary_ints =
   let
-    fun aux def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) =
-        aux def t1 andalso aux false t2
-      | aux def (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
-      | aux def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =
-        aux def t1 andalso aux false t2
-      | aux def (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
+    fun aux def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+      | aux def \<^Const_>\<open>Pure.imp for t1 t2\<close> = aux false t1 andalso aux def t2
+      | aux def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+      | aux def \<^Const_>\<open>implies for t1 t2\<close> = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
-      | aux def (t as Const (s, _)) =
-        (not def orelse t <> \<^const>\<open>Suc\<close>) andalso
+      | aux def (t as Const (s, _)) = (not def orelse t <> \<^Const>\<open>Suc\<close>) andalso
         not (member (op =)
                [\<^const_name>\<open>Abs_Frac\<close>, \<^const_name>\<open>Rep_Frac\<close>,
                 \<^const_name>\<open>nat_gcd\<close>, \<^const_name>\<open>nat_lcm\<close>,
@@ -143,7 +140,7 @@
       | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
       case t of
-        \<^const>\<open>Trueprop\<close> $ t1 => box_var_in_def new_Ts old_Ts t1 z
+        \<^Const_>\<open>Trueprop for t1\<close> => box_var_in_def new_Ts old_Ts t1 z
       | Const (s0, _) $ t1 $ _ =>
         if s0 = \<^const_name>\<open>Pure.eq\<close> orelse s0 = \<^const_name>\<open>HOL.eq\<close> then
           let
@@ -190,31 +187,29 @@
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>Pure.eq\<close>, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
-        \<^const>\<open>Pure.imp\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-        \<^const>\<open>Pure.conjunction\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>Trueprop\<close> $ t1 =>
-        \<^const>\<open>Trueprop\<close> $ do_term new_Ts old_Ts polar t1
-      | \<^const>\<open>Not\<close> $ t1 =>
-        \<^const>\<open>Not\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
+      | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+        \<^Const>\<open>Pure.imp for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+        \<^Const>\<open>Pure.conjunction for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>Trueprop for t1\<close> => \<^Const>\<open>Trueprop for \<open>do_term new_Ts old_Ts polar t1\<close>\<close>
+      | \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>\<close>
       | Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as \<^const_name>\<open>HOL.eq\<close>, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
-      | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.conj\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.disj\<close> $ do_term new_Ts old_Ts polar t1
-        $ do_term new_Ts old_Ts polar t2
-      | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
-        \<^const>\<open>HOL.implies\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
-        $ do_term new_Ts old_Ts polar t2
+      | \<^Const_>\<open>conj for t1 t2\<close> =>
+        \<^Const>\<open>conj for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>disj for t1 t2\<close> =>
+        \<^Const>\<open>disj for \<open>do_term new_Ts old_Ts polar t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+      | \<^Const_>\<open>implies for t1 t2\<close> =>
+        \<^Const>\<open>implies for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+          \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
       | Const (x as (s, T)) =>
         if is_descr s then
           do_descr s T
@@ -335,11 +330,11 @@
       case t of
         (t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2 =>
+      | (t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2 =>
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
       | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+      | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -402,11 +397,11 @@
                     | _ => I) t (K 0)
     fun aux Ts careful ((t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2) =
         aux_eq Ts careful true t0 t1 t2
-      | aux Ts careful ((t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2) =
+      | aux Ts careful ((t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2) =
         t0 $ aux Ts false t1 $ aux Ts careful t2
       | aux Ts careful ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2) =
         aux_eq Ts careful true t0 t1 t2
-      | aux Ts careful ((t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2) =
+      | aux Ts careful ((t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2) =
         t0 $ aux Ts false t1 $ aux Ts careful t2
       | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
       | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
@@ -417,13 +412,13 @@
           raise SAME ()
         else if axiom andalso is_Var t2 andalso
                 num_occs_of_var (dest_Var t2) = 1 then
-          \<^const>\<open>True\<close>
+          \<^Const>\<open>True\<close>
         else case strip_comb t2 of
           (* The first case is not as general as it could be. *)
           (Const (\<^const_name>\<open>PairBox\<close>, _),
                   [Const (\<^const_name>\<open>fst\<close>, _) $ Var z1,
                    Const (\<^const_name>\<open>snd\<close>, _) $ Var z2]) =>
-          if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^const>\<open>True\<close>
+          if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^Const>\<open>True\<close>
           else raise SAME ()
         | (Const (x as (s, T)), args) =>
           let
@@ -454,26 +449,22 @@
 
 (** Destruction of universal and existential equalities **)
 
-fun curry_assms (\<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close>
-                                   $ (\<^const>\<open>HOL.conj\<close> $ t1 $ t2)) $ t3) =
+fun curry_assms \<^Const_>\<open>Pure.imp for \<^Const>\<open>Trueprop for \<^Const_>\<open>conj for t1 t2\<close>\<close> t3\<close> =
     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
-  | curry_assms (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
-    \<^const>\<open>Pure.imp\<close> $ curry_assms t1 $ curry_assms t2
+  | curry_assms \<^Const_>\<open>Pure.imp for t1 t2\<close> = \<^Const>\<open>Pure.imp for \<open>curry_assms t1\<close> \<open>curry_assms t2\<close>\<close>
   | curry_assms t = t
 
 val destroy_universal_equalities =
   let
     fun aux prems zs t =
       case t of
-        \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => aux_implies prems zs t1 t2
+        \<^Const_>\<open>Pure.imp for t1 t2\<close> => aux_implies prems zs t1 t2
       | _ => Logic.list_implies (rev prems, t)
     and aux_implies prems zs t1 t2 =
       case t1 of
-        Const (\<^const_name>\<open>Pure.eq\<close>, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var z $ t') =>
-        aux_eq prems zs z t' t1 t2
-      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ Var z) =>
-        aux_eq prems zs z t' t1 t2
+        \<^Const_>\<open>Pure.eq _ for \<open>Var z\<close> t'\<close> => aux_eq prems zs z t' t1 t2
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var z\<close> t'\<close>\<close> => aux_eq prems zs z t' t1 t2
+      | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t' \<open>Var z\<close>\<close>\<close> => aux_eq prems zs z t' t1 t2
       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
     and aux_eq prems zs z t' t1 t2 =
       if not (member (op =) zs z) andalso
@@ -528,7 +519,7 @@
     fun kill [] [] ts = foldr1 s_conj ts
       | kill (s :: ss) (T :: Ts) ts =
         (case find_bound_assign ctxt (length ss) [] ts of
-           SOME (_, []) => \<^const>\<open>True\<close>
+           SOME (_, []) => \<^Const>\<open>True\<close>
          | SOME (arg_t, ts) =>
            kill ss Ts (map (subst_one_bound (length ss)
                                 (incr_bv (~1, length ss + 1, arg_t))) ts)
@@ -592,27 +583,27 @@
         case t of
           Const (s0 as \<^const_name>\<open>Pure.all\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
-          \<^const>\<open>Pure.imp\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
-          $ aux ss Ts js skolemizable polar t2
-        | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
-          \<^const>\<open>Pure.conjunction\<close> $ aux ss Ts js skolemizable polar t1
-          $ aux ss Ts js skolemizable polar t2
-        | \<^const>\<open>Trueprop\<close> $ t1 =>
-          \<^const>\<open>Trueprop\<close> $ aux ss Ts js skolemizable polar t1
-        | \<^const>\<open>Not\<close> $ t1 =>
-          \<^const>\<open>Not\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
+        | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+          \<^Const>\<open>Pure.imp for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+        | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+          \<^Const>\<open>Pure.conjunction for \<open>aux ss Ts js skolemizable polar t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+        | \<^Const_>\<open>Trueprop for t1\<close> =>
+          \<^Const>\<open>Trueprop for \<open>aux ss Ts js skolemizable polar t1\<close>\<close>
+        | \<^Const_>\<open>Not for t1\<close> =>
+          \<^Const>\<open>Not for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>\<close>
         | Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
         | Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
-        | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
+        | \<^Const_>\<open>conj for t1 t2\<close> =>
           s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
-        | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
+        | \<^Const_>\<open>disj for t1 t2\<close> =>
           s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
-        | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
-          \<^const>\<open>HOL.implies\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
-          $ aux ss Ts js skolemizable polar t2
+        | \<^Const_>\<open>implies for t1 t2\<close> =>
+          \<^Const>\<open>implies for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+            \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
         | (t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js skolemizable polar t2
         | Const (x as (s, T)) =>
@@ -622,8 +613,8 @@
             let
               val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
               val (pref, connective) =
-                if gfp then (lbfp_prefix, \<^const>\<open>HOL.disj\<close>)
-                else (ubfp_prefix, \<^const>\<open>HOL.conj\<close>)
+                if gfp then (lbfp_prefix, \<^Const>\<open>disj\<close>)
+                else (ubfp_prefix, \<^Const>\<open>conj\<close>)
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
                            |> aux ss Ts js skolemizable polar
               fun neg () = Const (pref ^ s, T)
@@ -653,10 +644,9 @@
 
 (** Function specialization **)
 
-fun params_in_equation (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = params_in_equation t2
-  | params_in_equation (\<^const>\<open>Trueprop\<close> $ t1) = params_in_equation t1
-  | params_in_equation (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _) =
-    snd (strip_comb t1)
+fun params_in_equation \<^Const_>\<open>Pure.imp for _ t2\<close> = params_in_equation t2
+  | params_in_equation \<^Const_>\<open>Trueprop for t1\<close> = params_in_equation t1
+  | params_in_equation \<^Const_>\<open>HOL.eq _ for t1 _\<close> = snd (strip_comb t1)
   | params_in_equation _ = []
 
 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
@@ -865,10 +855,8 @@
       if exists_subterm (curry (op aconv) u) def then NONE else SOME u
   in
     case t of
-      Const (\<^const_name>\<open>Pure.eq\<close>, _) $ (u as Free _) $ def => do_equals u def
-    | \<^const>\<open>Trueprop\<close>
-      $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (u as Free _) $ def) =>
-      do_equals u def
+      \<^Const_>\<open>Pure.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
+    | \<^Const_>\<open>Trueprop\<close> $ \<^Const_>\<open>HOL.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
     | _ => NONE
   end
 
@@ -917,7 +905,7 @@
     and add_def_axiom depth = add_axiom fst apfst true depth
     and add_nondef_axiom depth = add_axiom snd apsnd false depth
     and add_maybe_def_axiom depth t =
-      (if head_of t <> \<^const>\<open>Pure.imp\<close> then add_def_axiom
+      (if head_of t <> \<^Const>\<open>Pure.imp\<close> then add_def_axiom
        else add_nondef_axiom) depth t
     and add_eq_axiom depth t =
       (if is_constr_pattern_formula ctxt t then add_def_axiom
@@ -1104,10 +1092,10 @@
   case t of
     (t0 as Const (\<^const_name>\<open>All\<close>, T0)) $ Abs (s, T1, t1) =>
     (case t1 of
-       (t10 as \<^const>\<open>HOL.conj\<close>) $ t11 $ t12 =>
+       (t10 as \<^Const_>\<open>conj\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+     | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>Ex\<close>, T0)
                                      $ Abs (s, T1, t11))
      | t1 =>
@@ -1117,14 +1105,14 @@
          t0 $ Abs (s, T1, distribute_quantifiers t1))
   | (t0 as Const (\<^const_name>\<open>Ex\<close>, T0)) $ Abs (s, T1, t1) =>
     (case distribute_quantifiers t1 of
-       (t10 as \<^const>\<open>HOL.disj\<close>) $ t11 $ t12 =>
+       (t10 as \<^Const_>\<open>disj\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>HOL.implies\<close>) $ t11 $ t12 =>
+     | (t10 as \<^Const_>\<open>implies\<close>) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
                                      $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+     | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
        t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
                                      $ Abs (s, T1, t11))
      | t1 =>