src/HOL/Tools/Predicate_Compile/code_prolog.ML

             AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
       | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
 
 fun translate_literal ctxt constant_table t =
   case strip_comb t of
-    (Const (@{const_name "op ="}, _), [l, r]) =>
+    (Const (@{const_name HOL.eq}, _), [l, r]) =>
       let
         val l' = translate_term ctxt constant_table l
         val r' = translate_term ctxt constant_table r
       in
         (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r')