--- a/src/Pure/goal.ML Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/goal.ML Sat Mar 20 17:33:11 2010 +0100
@@ -129,7 +129,8 @@
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
val global_prop =
- cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+ cert (Term.map_types Logic.varifyT_global
+ (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
|> Thm.weaken_sorts (Variable.sorts_of ctxt);
val global_result = result |> Future.map
(Drule.flexflex_unique #>