src/HOL/simpdata.ML
 changeset 13600 9702c8636a7b parent 13568 6b12df05f358 child 13743 f8f9393be64c
```     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 @@