src/Provers/classical.ML
changeset 18989 a5c3bc6fd6b6
parent 18834 7e94af77cfce
child 19110 4bda27adcd2e
     1.1 --- a/src/Provers/classical.ML	Fri Feb 10 02:22:16 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Feb 10 02:22:19 2006 +0100
     1.3 @@ -675,10 +675,10 @@
     1.4    treatment of priority might get muddled up.*)
     1.5  fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
     1.6       CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
     1.7 -  let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
     1.8 -      val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
     1.9 -      val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
    1.10 -      val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
    1.11 +  let val safeIs' = fold rem_thm safeIs safeIs2
    1.12 +      val safeEs' = fold rem_thm safeEs safeEs2
    1.13 +      val hazIs' = fold rem_thm hazIs hazIs2
    1.14 +      val hazEs' = fold rem_thm hazEs hazEs2
    1.15        val cs1   = cs addSIs safeIs'
    1.16                       addSEs safeEs'
    1.17                       addIs  hazIs'