Modified mk_meta_eq to leave meta-equlities on unchanged.
Thus you may now add ==-thms to simpsets.

--- a/src/FOL/simpdata.ML	Thu May 19 17:06:24 1994 +0200
+++ b/src/FOL/simpdata.ML	Tue May 24 09:04:03 1994 +0200
@@ -72,7 +72,8 @@
 
 (*Make meta-equalities.  The operator below is Trueprop*)
 fun mk_meta_eq th = case concl_of th of
-    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
+    Const("==",_)$_$_           => th
+  | _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
   | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;