src/Pure/goal.ML
changeset 33768 bba9eac8aa25
parent 32788 a65deb8f9434
child 35021 c839a4c670c6
     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);