# HG changeset patch
# User wenzelm
# Date 1248005747 -7200
# Node ID f4b74cbecdafe5c59586a5b8bcf4660e1ae61f28
# Parent  6a46898aa805df59e7dc5c1871f6b23de7607008
future_result: explicitly impose Variable.sorts_of again;

diff -r 6a46898aa805 -r f4b74cbecdaf src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jul 19 14:14:25 2009 +0200
+++ b/src/Pure/goal.ML	Sun Jul 19 14:15:47 2009 +0200
@@ -120,14 +120,15 @@
     val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
 
     val global_prop =
-      Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
+      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.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
         Thm.generalize (map #1 tfrees, []) 0);
     val local_result =
-      Thm.future global_result (cert global_prop)
+      Thm.future global_result global_prop
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;