tuned;

--- a/src/Provers/classical.ML	Fri Feb 10 02:22:16 2006 +0100
+++ b/src/Provers/classical.ML	Fri Feb 10 02:22:19 2006 +0100
@@ -675,10 +675,10 @@
   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, swrappers, uwrappers, ...}) =
-  let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
-      val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
-      val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
-      val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
+  let val safeIs' = fold rem_thm safeIs safeIs2
+      val safeEs' = fold rem_thm safeEs safeEs2
+      val hazIs' = fold rem_thm hazIs hazIs2
+      val hazEs' = fold rem_thm hazEs hazEs2
       val cs1   = cs addSIs safeIs'
                      addSEs safeEs'
                      addIs  hazIs'

--- a/src/Pure/library.ML	Fri Feb 10 02:22:16 2006 +0100
+++ b/src/Pure/library.ML	Fri Feb 10 02:22:19 2006 +0100
@@ -925,8 +925,9 @@
 fun (x: string) mem_string xs = member (op =) xs x;
 
 fun x ins xs = insert (op =) x xs;
-fun (x:int) ins_int xs = insert (op =) x xs;
-fun (x:string) ins_string xs = insert (op =) x xs;
+fun (x: int) ins_int xs = insert (op =) x xs;
+fun (x: string) ins_string xs = insert (op =) x xs;
+
 
 (*union of sets represented as lists: no repetitions*)
 fun xs union [] = xs