diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Library/reflection.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -82,7 +82,7 @@
 fun rearrange congs =
   let
     fun P (_, th) =
-      let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
+      let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
       in can dest_Var l end
     val (yes,no) = List.partition P congs
   in no @ yes end