src/HOL/Tools/simpdata.ML

--- a/src/HOL/Tools/simpdata.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -43,7 +43,7 @@
 
 fun mk_eq th = case concl_of th
   (*expects Trueprop if not == *)
-  of Const (@{const_name "=="},_) $ _ $ _ => th
+  of Const (@{const_name Pure.eq},_) $ _ $ _ => th
    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
    | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
    | _ => th RS @{thm Eq_TrueI}