src/HOL/Tools/Datatype/datatype_codegen.ML

       let
         val ty = Type (tyco, map TFree vs);
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
+          (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (Attrib.empty_binding, def')) lthy;
         val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;