src/HOL/Tools/inductive_codegen.ML

   let
     val {intros, graph, eqns} = CodegenData.get thy;
     fun thyname_of s = (case optmod of
       NONE => Codegen.thyname_of_const thy s | SOME s => s);
   in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
-      SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+      SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
         (case head_of t of
           Const (s, _) =>
             CodegenData.put {intros = intros, graph = graph,
                eqns = eqns |> Symtab.map_default (s, [])
                  (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy

                     (iss ~~ args1)))
           end
         end)) (AList.lookup op = modes name)
 
   in (case strip_comb t of
-      (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
+      (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
         [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
         (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
     | (Const (name, _), args) => the_default default (mk_modes name args)
     | (Var ((name, _), _), args) => the (mk_modes name args)
     | (Free (name, _), args) => the (mk_modes name args)

           [Pretty.brk 1, str "| _ => DSeq.empty)"]
         else [str ")"])))
   end;
 
 fun modename module s (iss, is) gr =
-  let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
+  let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
     else mk_const_id module s gr
   in (space_implode "__"
     (mk_qual_id module id ::
       map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr')
   end;

   | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
       ([str name], gr)
   | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
       (case strip_comb t of
          (Const (name, _), args) =>
-           if name = @{const_name "op ="} orelse AList.defined op = modes name then
+           if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
              let
                val (args1, args2) = chop (length ms) args;
                val ((ps, mode_id), gr') = gr |> fold_map
                    (compile_expr thy defs dep module true modes) (ms ~~ args1)
                    ||>> modename module name mode;

       fun get_nparms s = if member (op =) names s then SOME nparms else
         Option.map #3 (get_clauses thy s);
 
       fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
             Prem ([t], Envir.beta_eta_contract u, true)
-        | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
+        | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
             Prem ([t, u], eq, false)
         | dest_prem (_ $ t) =
             (case strip_comb t of
               (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t
             | (c as Const (s, _), ts) =>