src/Sequents/prover.ML
changeset 20951 868120282837
parent 18708 4b3dadb4fe33
child 21428 f84cf8e9cad8
     1.1 --- a/src/Sequents/prover.ML	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/src/Sequents/prover.ML	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -33,14 +33,14 @@
     1.4  
     1.5  fun (Pack(safes,unsafes)) add_safes ths   = 
     1.6      let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
     1.7 -	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
     1.8 +	val ths' = subtract Drule.eq_thm_prop dups ths
     1.9      in
    1.10          Pack(sort (make_ord less) (ths'@safes), unsafes)
    1.11      end;
    1.12  
    1.13  fun (Pack(safes,unsafes)) add_unsafes ths = 
    1.14      let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
    1.15 -	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
    1.16 +	val ths' = subtract Drule.eq_thm_prop dups ths
    1.17      in
    1.18  	Pack(safes, sort (make_ord less) (ths'@unsafes))
    1.19      end;