# HG changeset patch
# User berghofe
# Date 1033395136 -7200
# Node ID 9702c8636a7b6bd0904a6f628806dc9cd3ed20db
# Parent  cfdf7e4cd0d20bd1a00edf533e5f29b613d9d9e0
Removed nRS again because extract_rews now takes care of preserving names.

diff -r cfdf7e4cd0d2 -r 9702c8636a7b src/HOL/simpdata.ML
--- 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])