# HG changeset patch
# User oheimb
# Date 891285318 -7200
# Node ID d2c41c8b545f356a974365baf4683315ac0a6671
# Parent  9b3293646b5dbd4253ea86b54dc8cd8aae12a07f
merge_cs now also merges safe and unsafe wrappers

diff -r 9b3293646b5d -r d2c41c8b545f src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Mar 30 21:14:04 1998 +0200
+++ b/src/Provers/classical.ML	Mon Mar 30 21:15:18 1998 +0200
@@ -72,8 +72,8 @@
   val addSaltern 	: claset * (string * (int -> tactic)) -> claset
   val addbefore 	: claset * (string * (int -> tactic)) -> claset
   val addaltern	 	: claset * (string * (int -> tactic)) -> claset
+  val appSWrappers	: claset -> wrapper
   val appWrappers	: claset -> wrapper
-  val appSWrappers	: claset -> wrapper
 
   val claset_ref_of_sg: Sign.sg -> claset ref
   val claset_ref_of: theory -> claset ref
@@ -539,7 +539,7 @@
      safeEs	= safeEs,
      hazIs	= hazIs,
      hazEs	= hazEs,
-     swrappers   = swrappers,
+     swrappers  = swrappers,
      uwrappers 	= (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
 	   | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
 		   overwrite (uwrappers, new_uwrapper)),
@@ -599,15 +599,19 @@
   treatment of priority might get muddled up.*)
 fun merge_cs
     (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
-     CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) =
+     CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,
+	swrappers, uwrappers, ...}) =
   let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
       val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
       val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
       val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
-  in cs addSIs safeIs'
-        addSEs safeEs'
-        addIs  hazIs'
-        addEs  hazEs'
+      val cs'   = cs addSIs safeIs'
+		     addSEs safeEs'
+		     addIs  hazIs'
+		     addEs  hazEs'
+      val cs''  = foldl (op addSWrapper) (cs' , swrappers);
+      val cs''' = foldl (op addWrapper ) (cs'', uwrappers);
+  in cs''' 
   end;