diff -r dea0d2cca822 -r d0385f2764d8 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 19 11:02:14 2010 +0200
@@ -111,7 +111,7 @@
 
 fun mk_meta_equation th =
   case prop_of th of
-    Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
+    Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}