Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/meta_simplifier.ML
changeset 11371 1d5d181b7e28
parent 11295 66925f23ac7f
child 11504 935f9e8de0d0 
--- a/src/Pure/meta_simplifier.ML	Sun Jun 10 08:03:35 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Jun 11 19:21:13 2001 +0200
@@ -802,7 +802,12 @@
         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
             (mk_implies (prem1, conc)) of
               None => None
-            | Some (thm, _) => Some (None, thm))
+            | Some (thm, _) => 
+                let val (prem, conc) = Drule.dest_implies (rhs_of thm)
+                in (case mut_impc (prems, prem, conc, mss) of
+                    None => Some (None, thm)
+                  | Some (x, thm') => Some (x, transitive thm thm'))
+                end handle TERM _ => Some (None, thm))
           | rebuild (Some thm2) =
             let val thm = disch1 thm2
             in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
isabelle