# HG changeset patch
# User wenzelm
# Date 1258648179 -3600
# Node ID bba9eac8aa2546bd2c4b48342974fcc1712de872
# Parent  f962c761a38f598d73e45bf049c742a85b3a0911
future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;

diff -r f962c761a38f -r bba9eac8aa25 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Nov 19 17:26:28 2009 +0100
+++ b/src/Pure/goal.ML	Thu Nov 19 17:29:39 2009 +0100
@@ -132,7 +132,8 @@
       cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
       |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     val global_result = result |> Future.map
-      (Thm.adjust_maxidx_thm ~1 #>
+      (Drule.flexflex_unique #>
+        Thm.adjust_maxidx_thm ~1 #>
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
         Thm.generalize (map #1 tfrees, []) 0);