--- a/src/Sequents/prover.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Sequents/prover.ML Mon Feb 26 23:18:24 2007 +0100
@@ -32,15 +32,15 @@
dups);
fun (Pack(safes,unsafes)) add_safes ths =
- let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
- val ths' = subtract Drule.eq_thm_prop dups ths
+ let val dups = warn_duplicates (gen_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 (gen_inter Drule.eq_thm_prop (ths,unsafes))
- val ths' = subtract Drule.eq_thm_prop dups ths
+ let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
+ val ths' = subtract Thm.eq_thm_prop dups ths
in
Pack(safes, sort (make_ord less) (ths'@unsafes))
end;