# HG changeset patch
# User lcp
# Date 783877939 -3600
# Node ID eb5b42442b14b0cdca15e788fbc0805896f03deb
# Parent  a1586fa1b755a8486c3e801f744b73aec858cfb8
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
result.

diff -r a1586fa1b755 -r eb5b42442b14 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Nov 03 16:39:41 1994 +0100
+++ b/src/Pure/goals.ML	Thu Nov 03 16:52:19 1994 +0100
@@ -139,7 +139,9 @@
       (*discharges assumptions from state in the order they appear in goal;
 	checks (if requested) that resulting theorem is equivalent to goal. *)
       fun mkresult (check,state) =
-        let val ngoals = nprems_of state
+        let val state = Sequence.hd (flexflex_rule state)
+	    		handle _ => state   (*smash flexflex pairs*)
+	    val ngoals = nprems_of state
             val th = implies_intr_list cAs state
             val {hyps,prop,sign=sign',...} = rep_thm th
         in  if not check then standard th