src/Pure/goal.ML
changeset 35845 e5980f0ad025
parent 35021 c839a4c670c6
child 36610 bafd82950e24
     1.1 --- a/src/Pure/goal.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Pure/goal.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -129,7 +129,8 @@
     1.4      val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
     1.5  
     1.6      val global_prop =
     1.7 -      cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
     1.8 +      cert (Term.map_types Logic.varifyT_global
     1.9 +        (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
    1.10        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
    1.11      val global_result = result |> Future.map
    1.12        (Drule.flexflex_unique #>