--- a/src/Sequents/prover.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Sequents/prover.ML Wed Oct 21 12:09:37 2009 +0200
@@ -31,14 +31,14 @@
dups);
fun (Pack(safes,unsafes)) add_safes ths =
- let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
+ let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
val ths' = subtract Thm.eq_thm_prop dups ths
in
Pack(sort (make_ord less) (ths'@safes), unsafes)
end;
fun (Pack(safes,unsafes)) add_unsafes ths =
- let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
+ let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
val ths' = subtract Thm.eq_thm_prop dups ths
in
Pack(safes, sort (make_ord less) (ths'@unsafes))