src/Pure/meta_simplifier.ML
changeset 11371 1d5d181b7e28
parent 11295 66925f23ac7f
child 11504 935f9e8de0d0
     1.1 --- a/src/Pure/meta_simplifier.ML	Sun Jun 10 08:03:35 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Jun 11 19:21:13 2001 +0200
     1.3 @@ -802,7 +802,12 @@
     1.4          fun rebuild None = (case rewritec (prover, sign, maxidx) mss
     1.5              (mk_implies (prem1, conc)) of
     1.6                None => None
     1.7 -            | Some (thm, _) => Some (None, thm))
     1.8 +            | Some (thm, _) => 
     1.9 +                let val (prem, conc) = Drule.dest_implies (rhs_of thm)
    1.10 +                in (case mut_impc (prems, prem, conc, mss) of
    1.11 +                    None => Some (None, thm)
    1.12 +                  | Some (x, thm') => Some (x, transitive thm thm'))
    1.13 +                end handle TERM _ => Some (None, thm))
    1.14            | rebuild (Some thm2) =
    1.15              let val thm = disch1 thm2
    1.16              in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of