# HG changeset patch
# User berghofe
# Date 992280073 -7200
# Node ID 1d5d181b7e2876af4c246f7bfa84480c34c8c551
# Parent  680946254afe7f513b9590786db4f8531ac9a7e5
Fixed bug in function rebuild.

diff -r 680946254afe -r 1d5d181b7e28 src/Pure/meta_simplifier.ML
--- 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