Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
result.

--- 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