src/HOL/Tools/Sledgehammer/metis_tactics.ML

       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
              (case strip_prefix_and_undo_ascii schematic_var_prefix v of
                   SOME w =>  mk_var(w, dummyT)
                 | NONE   => mk_var(v, dummyT))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
-            Const ("op =", HOLogic.typeT)
+            Const (@{const_name "op ="}, HOLogic.typeT)
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_undo_ascii const_prefix x of
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_undo_ascii fixed_var_prefix x of