diff -r df7aac8543c9 -r 3d1e7a199bdc src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Sequents/prover.ML	Tue May 07 14:26:32 2002 +0200
@@ -32,15 +32,15 @@
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
-    let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
-	val ths' = gen_rems eq_thm (ths,dups)
+    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
+	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
     in
         Pack(sort (make_ord less) (ths'@safes), unsafes)
     end;
 
 fun (Pack(safes,unsafes)) add_unsafes ths = 
-    let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
-	val ths' = gen_rems eq_thm (ths,dups)
+    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
+	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
     in
 	Pack(safes, sort (make_ord less) (ths'@unsafes))
     end;