src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

   | explode_interval max (Facts.From i) = i upto i + max - 1
   | explode_interval _ (Facts.Single i) = [i]
 
 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
 
-fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
-  | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
+fun is_rec_def (\<^const>\<open>Trueprop\<close> $ t) = is_rec_def t
+  | is_rec_def (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = is_rec_def t2
   | is_rec_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
   | is_rec_def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
   | is_rec_def _ = false
 
 fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms

           not (exists_subterm is_interesting_subterm t) then
         Boring
       else
         Interesting
 
-    fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
-      | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
+    fun interest_of_prop _ (\<^const>\<open>Trueprop\<close> $ t) = interest_of_bool t
+      | interest_of_prop Ts (\<^const>\<open>Pure.imp\<close> $ t $ u) =
         combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
       | interest_of_prop Ts (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) =
         if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
       | interest_of_prop Ts ((t as Const (\<^const_name>\<open>Pure.all\<close>, _)) $ u) =
         interest_of_prop Ts (t $ eta_expand Ts u 1)

         |> fold (add Intro) intros
         |> fold (add Inductive) spec_intros
       end
   end
 
-fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
+fun normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
     if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
-  | normalize_eq (@{const Trueprop} $ (t as @{const Not}
+  | normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as \<^const>\<open>Not\<close>
       $ ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2))) =
     if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
   | normalize_eq (Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2) =
     (if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1))
     |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)

   |> sort (int_ord o apply2 fst)
   |> map snd
 
 fun struct_induct_rule_on th =
   (case Logic.strip_horn (Thm.prop_of th) of
-    (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
+    (prems, \<^const>\<open>Trueprop\<close> $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
     if not (is_TVar ind_T) andalso length prems > 1 andalso
        exists (exists_subterm (curry (op aconv) p)) prems andalso
        not (exists (exists_subterm (curry (op aconv) a)) prems) then
       SOME (p_name, ind_T)
     else