src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML

     |> Thm.varifyT_global
   end;
 
 fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
   let
-    fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
-    fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
-    fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
+    fun mk_fcT_eq (t, u) = Const (\<^const_name>\<open>HOL.equal\<close>, fcT --> fcT --> HOLogic.boolT) $ t $ u;
+    fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, \<^term>\<open>True\<close>);
+    fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, \<^term>\<open>False\<close>);
 
     val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes;
 
     fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
     fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];

     fun add_def lthy =
       let
         fun mk_side const_name =
           Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
         val spec =
-          mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
+          mk_Trueprop_eq (mk_side \<^const_name>\<open>HOL.equal\<close>, mk_side \<^const_name>\<open>HOL.eq\<close>)
           |> Syntax.check_term lthy;
         val ((_, (_, raw_def)), lthy') =
           Specification.definition NONE [] [] (Binding.empty_atts, spec) lthy;
         val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
         val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;