# HG changeset patch
# User oheimb
# Date 889704936 -3600
# Node ID a25bb8a260ae63e5cfd196daed109e2eea5769c4
# Parent  7fcd106cb0ed57e51d7d80a10103a73baf22e1c6
improved coding of delWrapper and delSWrapper

diff -r 7fcd106cb0ed -r a25bb8a260ae src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Mar 12 13:13:19 1998 +0100
+++ b/src/Provers/classical.ML	Thu Mar 12 13:15:36 1998 +0100
@@ -556,9 +556,9 @@
      safeEs	= safeEs,
      hazIs	= hazIs,
      hazEs	= hazEs,
-     swrappers 	= (case assoc_string (swrappers, name) of None =>
-	   warning("safe wrapper "^ name ^" not in claset") | Some x => (); 
-		   filter_out (fn (n,f) => n = name) swrappers),
+     swrappers 	= let val (del,rest) = partition (fn (n,_) => n=name) swrappers
+               in if null del then (warning ("No such safe wrapper in claset: "
+				 ^ name); swrappers) else rest end,
      uwrappers  = uwrappers,
      safe0_netpair = safe0_netpair,
      safep_netpair = safep_netpair,
@@ -574,9 +574,9 @@
      hazIs	= hazIs,
      hazEs	= hazEs,
      swrappers  = swrappers,
-     uwrappers 	= (case assoc_string (uwrappers, name) of None =>
-	   warning("unsafe wrapper "^ name ^" not in claset") | Some x => (); 
-		   filter_out (fn (n,f) => n = name) uwrappers),
+     uwrappers 	= let val (del,rest) = partition (fn (n,_) => n=name) uwrappers
+             in if null del then (warning ("No such unsafe wrapper in claset: "
+				^ name); uwrappers) else rest end,
      safe0_netpair = safe0_netpair,
      safep_netpair = safep_netpair,
      haz_netpair = haz_netpair,