# HG changeset patch
# User berghofe
# Date 1033396664 -7200
# Node ID 2f121149acfe7d4b596cbe98313dd6ab13d7d8f4
# Parent  528f7489a403f95ad153d2478863ca7f91bbdff6
Removed nRS again because extract_rews now takes care of preserving names.

diff -r 528f7489a403 -r 2f121149acfe src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Sep 30 16:36:57 2002 +0200
+++ b/src/Pure/drule.ML	Mon Sep 30 16:37:44 2002 +0200
@@ -6,7 +6,7 @@
 Derived rules and other operations on theorems.
 *)
 
-infix 0 RS nRS RSN RL RLN MRS MRL OF COMP;
+infix 0 RS RSN RL RLN MRS MRL OF COMP;
 
 signature BASIC_DRULE =
 sig
@@ -45,7 +45,6 @@
   val assume_ax         : theory -> string -> thm
   val RSN               : thm * (int * thm) -> thm
   val RS                : thm * thm -> thm
-  val nRS               : thm * thm -> thm
   val RLN               : thm list * (int * thm list) -> thm list
   val RL                : thm list * thm list -> thm list
   val MRS               : thm list * thm -> thm
@@ -458,10 +457,6 @@
 (*resolution: P==>Q, Q==>R gives P==>R. *)
 fun tha RS thb = tha RSN (1,thb);
 
-(* preserves the name of the thm on the LEFT: *)
-fun th nRS rl = Thm.name_thm (Thm.name_of_thm th, th RS rl)
-
-
 (*For joining lists of rules*)
 fun thas RLN (i,thbs) =
   let val resolve = biresolution false (map (pair false) thas) i