Removed nRS again because extract_rews now takes care of preserving names.
authorberghofe
Mon Sep 30 16:12:16 2002 +0200 (2002-09-30)
changeset 136009702c8636a7b
parent 13599 cfdf7e4cd0d2
child 13601 fd3e3d6b37b2
Removed nRS again because extract_rews now takes care of preserving names.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Mon Sep 30 16:10:32 2002 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Sep 30 16:12:16 2002 +0200
     1.3 @@ -136,18 +136,18 @@
     1.4  
     1.5  (*Make meta-equalities.  The operator below is Trueprop*)
     1.6  
     1.7 -fun mk_meta_eq r = r nRS eq_reflection;
     1.8 +fun mk_meta_eq r = r RS eq_reflection;
     1.9  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    1.10  
    1.11  fun mk_eq th = case concl_of th of
    1.12          Const("==",_)$_$_       => th
    1.13      |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    1.14 -    |   _$(Const("Not",_)$_)    => th nRS Eq_FalseI
    1.15 -    |   _                       => th nRS Eq_TrueI;
    1.16 +    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    1.17 +    |   _                       => th RS Eq_TrueI;
    1.18  (* Expects Trueprop(.) if not == *)
    1.19  
    1.20  fun mk_eq_True r =
    1.21 -  Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
    1.22 +  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
    1.23  
    1.24  (*Congruence rules for = (instead of ==)*)
    1.25  fun mk_meta_cong rl =
    1.26 @@ -204,7 +204,7 @@
    1.27               (case head_of p of
    1.28                  Const(a,_) =>
    1.29                    (case assoc(pairs,a) of
    1.30 -                     Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
    1.31 +                     Some(rls) => flat (map atoms ([th] RL rls))
    1.32                     | None => [th])
    1.33                | _ => [th])
    1.34           | _ => [th])