diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Aug 19 11:02:14 2010 +0200
@@ -308,7 +308,7 @@
                   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)