future_result: explicitly impose Variable.sorts_of again;
authorwenzelm
Sun Jul 19 14:15:47 2009 +0200 (2009-07-19)
changeset 32056f4b74cbecdaf
parent 32055 6a46898aa805
child 32057 371aacbbd6ef
future_result: explicitly impose Variable.sorts_of again;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Sun Jul 19 14:14:25 2009 +0200
     1.2 +++ b/src/Pure/goal.ML	Sun Jul 19 14:15:47 2009 +0200
     1.3 @@ -120,14 +120,15 @@
     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 -      Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
     1.8 +      cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
     1.9 +      |> Thm.weaken_sorts (Variable.sorts_of ctxt);
    1.10      val global_result = result |> Future.map
    1.11        (Thm.adjust_maxidx_thm ~1 #>
    1.12          Drule.implies_intr_list assms #>
    1.13          Drule.forall_intr_list fixes #>
    1.14          Thm.generalize (map #1 tfrees, []) 0);
    1.15      val local_result =
    1.16 -      Thm.future global_result (cert global_prop)
    1.17 +      Thm.future global_result global_prop
    1.18        |> Thm.instantiate (instT, [])
    1.19        |> Drule.forall_elim_list fixes
    1.20        |> fold (Thm.elim_implies o Thm.assume) assms;