src/Pure/meta_simplifier.ML
changeset 18470 19be817913c4
parent 18208 dbdcf366db53
child 18573 0ee7eab8c845
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 22 00:28:58 2005 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 22 00:29:00 2005 +0100
     1.3 @@ -1100,7 +1100,7 @@
     1.4                val (rrs', asm') = rules_of_prem ss prem'
     1.5              in mut_impc prems concl rrss asms (prem' :: prems')
     1.6                (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
     1.7 -                (Drule.imp_cong' eqn (reflexive (Drule.list_implies
     1.8 +                (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
     1.9                    (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1
    1.10              end
    1.11  
    1.12 @@ -1114,13 +1114,13 @@
    1.13         in (case botc skel0 ss1 conc of
    1.14             NONE => (case thm1 of
    1.15                 NONE => NONE
    1.16 -             | SOME thm1' => SOME (Drule.imp_cong' thm1' (reflexive conc)))
    1.17 +             | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
    1.18           | SOME thm2 =>
    1.19             let val thm2' = disch false (prem1, thm2)
    1.20             in (case thm1 of
    1.21                 NONE => SOME thm2'
    1.22               | SOME thm1' =>
    1.23 -                 SOME (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2'))
    1.24 +                 SOME (transitive (Drule.imp_cong_rule thm1' (reflexive conc)) thm2'))
    1.25             end)
    1.26         end
    1.27