diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -111,7 +111,7 @@
 
 fun mk_meta_equation th =
   case prop_of th of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -217,7 +217,7 @@
    @{const_name "==>"},
    @{const_name Trueprop},
    @{const_name Not},
-   @{const_name "op ="},
+   @{const_name HOL.eq},
    @{const_name HOL.implies},
    @{const_name All},
    @{const_name Ex},