future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
authorwenzelm
Thu Nov 19 17:29:39 2009 +0100 (2009-11-19)
changeset 33768bba9eac8aa25
parent 33767 f962c761a38f
child 33769 6d8630fab26a
future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Thu Nov 19 17:26:28 2009 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Nov 19 17:29:39 2009 +0100
     1.3 @@ -132,7 +132,8 @@
     1.4        cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
     1.5        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     1.6      val global_result = result |> Future.map
     1.7 -      (Thm.adjust_maxidx_thm ~1 #>
     1.8 +      (Drule.flexflex_unique #>
     1.9 +        Thm.adjust_maxidx_thm ~1 #>
    1.10          Drule.implies_intr_list assms #>
    1.11          Drule.forall_intr_list fixes #>
    1.12          Thm.generalize (map #1 tfrees, []) 0);