# HG changeset patch
# User nipkow
# Date 1032444027 -7200
# Node ID 6b12df05f3589e4463be3cfb24880f5a4b0a18ca
# Parent  7f5bf04095bd41796500726552c9815dc2805967
preserve names of rewrite rules when transforming them

diff -r 7f5bf04095bd -r 6b12df05f358 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Sep 18 18:19:43 2002 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 19 16:00:27 2002 +0200
@@ -136,18 +136,18 @@
 
 (*Make meta-equalities.  The operator below is Trueprop*)
 
-fun mk_meta_eq r = r RS eq_reflection;
+fun mk_meta_eq r = r nRS 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 RS Eq_FalseI
-    |   _                       => th RS Eq_TrueI;
-(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+    |   _$(Const("Not",_)$_)    => th nRS Eq_FalseI
+    |   _                       => th nRS Eq_TrueI;
+(* Expects Trueprop(.) if not == *)
 
 fun mk_eq_True r =
-  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
+  Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
 
 (*Congruence rules for = (instead of ==)*)
 fun mk_meta_cong rl =
@@ -188,21 +188,15 @@
 val Addsplits        = Splitter.Addsplits;
 val Delsplits        = Splitter.Delsplits;
 
-(*In general it seems wrong to add distributive laws by default: they
-  might cause exponential blow-up.  But imp_disjL has been in for a while
-  and cannot be removed without affecting existing proofs.  Moreover,
-  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
-  grounds that it allows simplification of R in the two cases.*)
-
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
    ("If", [if_bool_eq_conj RS iffD1])];
 
-(* ###FIXME: move to Provers/simplifier.ML
+(*
 val mk_atomize:      (string * thm list) list -> thm -> thm list
+looks too specific to move it somewhere else
 *)
-(* ###FIXME: move to Provers/simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of
@@ -210,7 +204,7 @@
              (case head_of p of
                 Const(a,_) =>
                   (case assoc(pairs,a) of
-                     Some(rls) => flat (map atoms ([th] RL rls))
+                     Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
                    | None => [th])
               | _ => [th])
          | _ => [th])
@@ -237,6 +231,12 @@
     setmkeqTrue mk_eq_True
     setmkcong mk_meta_cong;
 
+(*In general it seems wrong to add distributive laws by default: they
+  might cause exponential blow-up.  But imp_disjL has been in for a while
+  and cannot be removed without affecting existing proofs.  Moreover,
+  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
+  grounds that it allows simplification of R in the two cases.*)
+
 val HOL_ss =
     HOL_basic_ss addsimps
      ([triv_forall_equality, (* prunes params *)