# HG changeset patch
# User paulson
# Date 858763389 -3600
# Node ID cc4c816dafdc58db48804f8c0954dab52bf3467d
# Parent  dfcd1b00f29421646b89f799eb3d0848fddb3922
delrules now deletes ALL occurrences of a rule, since it may appear in any of
the four lists.

diff -r dfcd1b00f294 -r cc4c816dafdc src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Mar 18 18:20:52 1997 +0100
+++ b/src/Provers/classical.ML	Wed Mar 19 10:23:09 1997 +0100
@@ -240,16 +240,19 @@
 
 val delete = delete_tagged_list o joinrules;
 
+val mem_thm = gen_mem eq_thm
+and rem_thm = gen_rem eq_thm;
+
 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   is still allowed.*)
 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
-       if gen_mem eq_thm (th, safeIs) then 
+       if mem_thm (th, safeIs) then 
 	 warning ("rule already in claset as Safe Intr\n" ^ string_of_thm th)
-  else if gen_mem eq_thm (th, safeEs) then
+  else if mem_thm (th, safeEs) then
          warning ("rule already in claset as Safe Elim\n" ^ string_of_thm th)
-  else if gen_mem eq_thm (th, hazIs) then 
+  else if mem_thm (th, hazIs) then 
          warning ("rule already in claset as unsafe Intr\n" ^ string_of_thm th)
-  else if gen_mem eq_thm (th, hazEs) then 
+  else if mem_thm (th, hazEs) then 
          warning ("rule already in claset as unsafe Elim\n" ^ string_of_thm th)
   else ();
 
@@ -258,7 +261,7 @@
 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
 	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
 	   th)  =
-  if gen_mem eq_thm (th, safeIs) then 
+  if mem_thm (th, safeIs) then 
 	 (warning ("ignoring duplicate Safe Intr\n" ^ string_of_thm th);
 	  cs)
   else
@@ -282,7 +285,7 @@
 fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
 		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
 	   th)  =
-  if gen_mem eq_thm (th, safeEs) then 
+  if mem_thm (th, safeEs) then 
 	 (warning ("ignoring duplicate Safe Elim\n" ^ string_of_thm th);
 	  cs)
   else
@@ -316,7 +319,7 @@
 fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
 	  th)=
-  if gen_mem eq_thm (th, hazIs) then 
+  if mem_thm (th, hazIs) then 
 	 (warning ("ignoring duplicate unsafe Intr\n" ^ string_of_thm th);
 	  cs)
   else
@@ -338,7 +341,7 @@
 fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
 		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
 	  th) =
-  if gen_mem eq_thm (th, hazEs) then 
+  if mem_thm (th, hazEs) then 
 	 (warning ("ignoring duplicate unsafe Elim\n" ^ string_of_thm th);
 	  cs)
   else
@@ -367,77 +370,85 @@
      Working out what to delete, requires repeating much of the code used
 	to insert.
      Separate functions delSI, etc., are not exported; instead delrules
-        searches in all the lists and chooses the relevant delXX function.
+        searches in all the lists and chooses the relevant delXX functions.
 ***)
 
-fun delSI (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
-               safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
-            th) =
-  let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
-  in CS{safeIs	= gen_rem eq_thm (safeIs,th),
-        safe0_netpair = delete (safe0_rls, []) safe0_netpair,
-	safep_netpair = delete (safep_rls, []) safep_netpair,
-	safeEs	= safeEs,
-	hazIs	= hazIs,
-	hazEs	= hazEs,
-	uwrapper     = uwrapper,
-	swrapper     = swrapper,
-	haz_netpair  = haz_netpair,
-	dup_netpair  = dup_netpair}
-  end;
+fun delSI th 
+          (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
+		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
+ if mem_thm (th, safeIs) then
+   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
+   in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
+	 safep_netpair = delete (safep_rls, []) safep_netpair,
+	 safeIs	= rem_thm (safeIs,th),
+	 safeEs	= safeEs,
+	 hazIs	= hazIs,
+	 hazEs	= hazEs,
+	 uwrapper     = uwrapper,
+	 swrapper     = swrapper,
+	 haz_netpair  = haz_netpair,
+	 dup_netpair  = dup_netpair}
+   end
+ else cs;
 
-fun delSE (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
-	       safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
-            th) =
-  let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
-  in CS{safeEs	= gen_rem eq_thm (safeEs,th),
-        safe0_netpair = delete ([], safe0_rls) safe0_netpair,
-	safep_netpair = delete ([], safep_rls) safep_netpair,
-	safeIs	= safeIs,
-	hazIs	= hazIs,
-	hazEs	= hazEs,
-	uwrapper     = uwrapper,
-	swrapper     = swrapper,
-	haz_netpair  = haz_netpair,
-	dup_netpair  = dup_netpair}
-  end;
+fun delSE th
+          (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
+	            safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
+ if mem_thm (th, safeEs) then
+   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
+   in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
+	 safep_netpair = delete ([], safep_rls) safep_netpair,
+	 safeIs	= safeIs,
+	 safeEs	= rem_thm (safeEs,th),
+	 hazIs	= hazIs,
+	 hazEs	= hazEs,
+	 uwrapper     = uwrapper,
+	 swrapper     = swrapper,
+	 haz_netpair  = haz_netpair,
+	 dup_netpair  = dup_netpair}
+   end
+ else cs;
 
 
-fun delI (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
-	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
-	   th) =
-     CS{hazIs	= gen_rem eq_thm (hazIs,th),
-	haz_netpair = delete ([th], []) haz_netpair,
+fun delI th
+         (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
+	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
+ if mem_thm (th, hazIs) then
+     CS{haz_netpair = delete ([th], []) haz_netpair,
 	dup_netpair = delete ([dup_intr th], []) dup_netpair,
 	safeIs 	= safeIs, 
 	safeEs	= safeEs,
+	hazIs	= rem_thm (hazIs,th),
 	hazEs	= hazEs,
 	uwrapper      = uwrapper,
 	swrapper      = swrapper,
 	safe0_netpair = safe0_netpair,
-	safep_netpair = safep_netpair};
+	safep_netpair = safep_netpair}
+ else cs;
 
-fun delE (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
-	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
-	   th) =
-     CS{hazEs	= gen_rem eq_thm (hazEs,th),
-	haz_netpair = delete ([], [th]) haz_netpair,
+fun delE th
+	 (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
+	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
+ if mem_thm (th, hazEs) then
+     CS{haz_netpair = delete ([], [th]) haz_netpair,
 	dup_netpair = delete ([], [dup_elim th]) dup_netpair,
 	safeIs	= safeIs, 
 	safeEs	= safeEs,
 	hazIs	= hazIs,
+	hazEs	= rem_thm (hazEs,th),
 	uwrapper      = uwrapper,
 	swrapper      = swrapper,
 	safe0_netpair = safe0_netpair,
-	safep_netpair = safep_netpair};
+	safep_netpair = safep_netpair}
+ else cs;
 
+(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) =
-       if gen_mem eq_thm (th, safeIs) then delSI(cs,th)
-  else if gen_mem eq_thm (th, safeEs) then delSE(cs,th)
-  else if gen_mem eq_thm (th, hazIs) then delI(cs,th)
-  else if gen_mem eq_thm (th, hazEs) then delE(cs,th)
-  else (warning ("rule not in claset\n" ^ (string_of_thm th)); 
-	cs);
+       if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
+	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) 
+       then delSI th (delSE th (delI th (delE th cs)))
+       else (warning ("rule not in claset\n" ^ (string_of_thm th)); 
+	     cs);
 
 val op delrules = foldl delrule;