src/HOL/Tools/Nitpick/nitpick_hol.ML

   if String.isPrefix nitpick_prefix s then
     case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
   else
     s
 
-fun s_conj (t1, @{const True}) = t1
-  | s_conj (@{const True}, 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 False} orelse t2 = @{const False} then @{const False}
+    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 False}) = t1
-  | s_disj (@{const False}, 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 True} orelse t2 = @{const True} then @{const True}
+    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)) =
     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   | strip_connective _ t = [t]
 
 fun strip_any_connective (t as (t0 $ _ $ _)) =
-    if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
+    if t0 = \<^const>\<open>HOL.conj\<close> orelse t0 = \<^const>\<open>HOL.disj\<close> then
       (strip_connective t0 t, t0)
     else
-      ([t], @{const Not})
-  | strip_any_connective t = ([t], @{const Not})
-val conjuncts_of = strip_connective @{const HOL.conj}
-val disjuncts_of = strip_connective @{const HOL.disj}
+      ([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>
 
 (* 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
    well. *)
 val built_in_consts =

     let
       val {qtyp, equiv_rel, equiv_thm, ...} =
         the (Quotient_Info.lookup_quotients thy s)
       val partial =
         case Thm.prop_of equiv_thm of
-          @{const Trueprop} $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
-        | @{const Trueprop} $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
+          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
+        | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
         | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
                                    \relation theorem"
       val Ts' = qtyp |> dest_Type |> snd
     in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end
   | equiv_relation_for_quot_type _ T =

   let
     fun close_up zs zs' =
       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 Pure.imp} $ t1 $ t2) =
+    fun aux zs (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
         let val zs' = Term.add_vars t1 zs in
           close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
         end
       | aux zs t = close_up zs (Term.add_vars t zs) t
   in aux [] end
 
 fun distinctness_formula T =
   all_distinct_unordered_pairs_of
-  #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
-  #> List.foldr (s_conj o swap) @{const True}
+  #> 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)
 
 fun uncached_data_type_constrs ({ctxt, ...} : hol_context) (T as Type (s, _)) =

                [(\<^const_name>\<open>Quot\<close>, rep_type_for_quot_type ctxt T --> T)]
              else case typedef_info ctxt s of
                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 Zero_Rep}, dest_Const @{const Suc_Rep}]
+               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 _ _ = []
 
 fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T =
   case AList.lookup (op =) (!constr_cache) T of

 
 fun s_betapply _ (t1 as Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1', t2) =
     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 True} $ t1', _) = t1'
-  | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ @{const False} $ _, 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) =
     let val body_T' = range_type body_T in
       Const (\<^const_name>\<open>Let\<close>, bound_T --> (bound_T --> body_T') --> body_T')

   in aux Ts t handle Same.SAME => t end
 
 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 Not} $ 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 True})
+      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 True}
-    else if is_nonfree_constr ctxt x' then @{const False}
+    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)
 
 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   let val (arg_Ts, dataT) = strip_type T in

 
 (* This function is designed to work for both real definition axioms and
    simplification rules (equational specifications). *)
 fun term_under_def t =
   case t of
-    @{const Pure.imp} $ _ $ t2 => term_under_def t2
+    \<^const>\<open>Pure.imp\<close> $ _ $ t2 => term_under_def t2
   | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => term_under_def t1
-  | @{const Trueprop} $ 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
   | Abs (_, _, t') => term_under_def t'
   | t1 $ _ => term_under_def t1
   | _ => t
 

       | aux (c as Const (\<^const_name>\<open>Pure.type\<close>, _)) (SOME t) = SOME (lambda c t)
       | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
         Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => (t1, t2)
-      | @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
+      | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
         (t1, t2)
       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
     val args = strip_comb lhs |> snd
   in fold_rev aux args (SOME rhs) end
 

 
 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 Pure.imp} $ _ $ t2 => lhs_of_equation t2
-  | @{const Trueprop} $ t1 => lhs_of_equation 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 HOL.implies} $ _ $ t2 => lhs_of_equation t2
+  | \<^const>\<open>HOL.implies\<close> $ _ $ t2 => lhs_of_equation t2
   | _ => NONE
 
 fun is_constr_pattern _ (Bound _) = true
   | is_constr_pattern _ (Var _) = true
   | is_constr_pattern ctxt t =

       |> map (fn (func_t, x) =>
                  (constr_case_body ctxt (dataT :: Ts)
                                    (incr_boundvars 1 func_t, x),
                   discriminate_value hol_ctxt x (Bound 0)))
       |> AList.group (op aconv)
-      |> map (apsnd (List.foldl s_disj @{const False}))
+      |> 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 False}, @{const True}] 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 True}, head_t2)] => head_t2
-        | [_, (@{const False}, head_t2)] => @{const Not} $ head_t2
+        | [_, (\<^const>\<open>True\<close>, head_t2)] => head_t2
+        | [_, (\<^const>\<open>False\<close>, head_t2)] => \<^const>\<open>Not\<close> $ head_t2
         | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
       else
-        @{const True} |> 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
   |> absdummy dataT
 

     val j = maxidx_of_term t + 1
     val (prems, concl) = Logic.strip_horn t
   in
     Logic.list_implies (prems,
         case concl of
-          @{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
+          \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
                                $ t1 $ t2) =>
-          @{const Trueprop} $ extensional_equal j T t1 t2
-        | @{const Trueprop} $ t' =>
-          @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
+          \<^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 Trueprop} $ extensional_equal j T t1 t2
+          \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
         | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
                          quote (Syntax.string_of_term ctxt t));
                 raise SAME ()))
     |> SOME
   end

          (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
                                  cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst
   end
 
 fun ground_theorem_table thy =
-  fold ((fn @{const Trueprop} $ t1 =>
+  fold ((fn \<^const>\<open>Trueprop\<close> $ t1 =>
             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
 
 fun ersatz_table ctxt =
  #ersatz_table (Data.get (Context.Proof ctxt))

     val normal_y = normal_fun $ y_var
     val is_unknown_t = Const (\<^const_name>\<open>is_unknown\<close>, rep_T --> bool_T)
   in
     [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
      Logic.list_implies
-         ([@{const Not} $ (is_unknown_t $ normal_x),
-           @{const Not} $ (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 Not} $ (is_unknown_t $ normal_x)),
-           HOLogic.mk_Trueprop (@{const Not} $ 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
 
 fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T =
   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 bisim_iterator_max}
+    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)
       $ Abs ("m", iter_T, HOLogic.eq_const iter_T $ (suc_const iter_T $ Bound 0) $ n_var)
     val x_var = Var (("x", 0), T)

           val tuple_T = HOLogic.mk_tupleT arg_Ts
           val j = length arg_Ts
           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 HOL.conj} $ t1 $ t2) =
-              @{const HOL.conj} $ repair_rec j t1 $ repair_rec j 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 t =
               let val (head, args) = strip_comb t in
                 if head = Bound j then
                   HOLogic.eq_const tuple_T $ Bound j
                   $ mk_flat_tuple tuple_T args

                   t
               end
           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 False}
+          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 False}
+                               |> 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,
            Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
                               |> ap_n_split (length arg_Ts) tuple_T bool_T))

     [] => (case def_props_for_const thy psimp_table x of
              [] => (if is_inductive_pred hol_ctxt x then
                       [inductive_pred_axiom hol_ctxt x]
                     else case def_of_const thy def_tables x of
                       SOME def =>
-                      @{const Trueprop} $ HOLogic.mk_eq (Const x, def)
+                      \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
                       |> equationalize_term ctxt "" |> the |> single
                     | NONE => [])
            | psimps => psimps)
   | simps => simps
 
 fun is_equational_fun_surely_complete hol_ctxt x =
   case equational_fun_axioms hol_ctxt x of
-    [@{const Trueprop} $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
+    [\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
     strip_comb t1 |> snd |> forall is_Var
   | _ => false
 
 (** Type preprocessing **)