src/Sequents/prover.ML
changeset 22360 26ead7ed4f4b
parent 21428 f84cf8e9cad8
child 26928 ca87aff1ad2d
     1.1 --- a/src/Sequents/prover.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/Sequents/prover.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -32,15 +32,15 @@
     1.4         dups);
     1.5  
     1.6  fun (Pack(safes,unsafes)) add_safes ths   = 
     1.7 -    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
     1.8 -	val ths' = subtract Drule.eq_thm_prop dups ths
     1.9 +    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
    1.10 +	val ths' = subtract Thm.eq_thm_prop dups ths
    1.11      in
    1.12          Pack(sort (make_ord less) (ths'@safes), unsafes)
    1.13      end;
    1.14  
    1.15  fun (Pack(safes,unsafes)) add_unsafes ths = 
    1.16 -    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
    1.17 -	val ths' = subtract Drule.eq_thm_prop dups ths
    1.18 +    let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes))
    1.19 +	val ths' = subtract Thm.eq_thm_prop dups ths
    1.20      in
    1.21  	Pack(safes, sort (make_ord less) (ths'@unsafes))
    1.22      end;