Removed nRS again because extract_rews now takes care of preserving names.

--- a/src/HOL/simpdata.ML	Mon Sep 30 16:10:32 2002 +0200
+++ b/src/HOL/simpdata.ML	Mon Sep 30 16:12:16 2002 +0200
@@ -136,18 +136,18 @@
 
 (*Make meta-equalities.  The operator below is Trueprop*)
 
-fun mk_meta_eq r = r nRS eq_reflection;
+fun mk_meta_eq r = r RS eq_reflection;
 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
 
 fun mk_eq th = case concl_of th of
         Const("==",_)$_$_       => th
     |   _$(Const("op =",_)$_$_) => mk_meta_eq th
-    |   _$(Const("Not",_)$_)    => th nRS Eq_FalseI
-    |   _                       => th nRS Eq_TrueI;
+    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
+    |   _                       => th RS Eq_TrueI;
 (* Expects Trueprop(.) if not == *)
 
 fun mk_eq_True r =
-  Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
+  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
 
 (*Congruence rules for = (instead of ==)*)
 fun mk_meta_cong rl =
@@ -204,7 +204,7 @@
              (case head_of p of
                 Const(a,_) =>
                   (case assoc(pairs,a) of
-                     Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
+                     Some(rls) => flat (map atoms ([th] RL rls))
                    | None => [th])
               | _ => [th])
          | _ => [th])