--- 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}