src/HOL/Tools/code_evaluation.ML

 fun certify_eval ctxt value conv ct =
   let
     val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
     val t = Thm.term_of ct;
     val T = fastype_of t;
-    val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
+    val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
   in case value ctxt t
    of NONE => Thm.reflexive ct
     | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
         handle THM _ =>
           error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)

 fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
   Code_Runtime.dynamic_holds_conv;
 
 fun static_conv ctxt consts Ts =
   let
-    val eqs = "==" :: @{const_name HOL.eq} ::
+    val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
       map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
-        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
+        (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
     val value = static_value ctxt consts Ts;
     val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
   in
     fn ctxt' => certify_eval ctxt' value holds
   end;