src/Sequents/prover.ML
changeset 13105 3d1e7a199bdc
parent 12311 ce5f9e61c037
child 16458 4c6fd0c01d28
     1.1 --- a/src/Sequents/prover.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Sequents/prover.ML	Tue May 07 14:26:32 2002 +0200
     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 eq_thm (ths,safes))
     1.8 -	val ths' = gen_rems eq_thm (ths,dups)
     1.9 +    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
    1.10 +	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
    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 eq_thm (ths,unsafes))
    1.17 -	val ths' = gen_rems eq_thm (ths,dups)
    1.18 +    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
    1.19 +	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
    1.20      in
    1.21  	Pack(safes, sort (make_ord less) (ths'@unsafes))
    1.22      end;