Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed bug in function rebuild.
authorberghofe
Mon, 11 Jun 2001 19:21:13 +0200
changeset 11371 1d5d181b7e28
parent 11370 680946254afe
child 11372 648795477bb5
Fixed bug in function rebuild.
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- 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