src/Provers/classical.ML
changeset 13105 3d1e7a199bdc
parent 12401 4363432ef0cd
child 13525 cafd1f98d658
     1.1 --- a/src/Provers/classical.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -310,8 +310,8 @@
     1.4  fun delete x = delete_tagged_list (joinrules x);
     1.5  fun delete' x = delete_tagged_list (joinrules' x);
     1.6  
     1.7 -val mem_thm = gen_mem eq_thm
     1.8 -and rem_thm = gen_rem eq_thm;
     1.9 +val mem_thm = gen_mem Drule.eq_thm_prop
    1.10 +and rem_thm = gen_rem Drule.eq_thm_prop;
    1.11  
    1.12  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    1.13    is still allowed.*)
    1.14 @@ -601,10 +601,10 @@
    1.15    treatment of priority might get muddled up.*)
    1.16  fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
    1.17       CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
    1.18 -  let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
    1.19 -      val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
    1.20 -      val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
    1.21 -      val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
    1.22 +  let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
    1.23 +      val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
    1.24 +      val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
    1.25 +      val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
    1.26        val cs1   = cs addSIs safeIs'
    1.27                       addSEs safeEs'
    1.28                       addIs  hazIs'