1.1 --- a/src/Pure/goal.ML	Thu Dec 04 23:00:27 2008 +0100
     1.2 +++ b/src/Pure/goal.ML	Thu Dec 04 23:00:58 2008 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_result: thm -> thm
     1.7 -  val future_result: Proof.context -> (unit -> thm) -> term -> thm
     1.8 +  val future_result: Proof.context -> thm future -> term -> thm
     1.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    1.12 @@ -116,11 +116,11 @@
    1.13  
    1.14      val global_prop =
    1.15        Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
    1.16 -    val global_result =
    1.17 -      Thm.generalize (map #1 tfrees, []) 0 o
    1.18 -      Drule.forall_intr_list fixes o
    1.19 -      Drule.implies_intr_list assms o
    1.20 -      Thm.adjust_maxidx_thm ~1 o result;
    1.21 +    val global_result = result |> Future.map
    1.22 +      (Thm.adjust_maxidx_thm ~1 #>
    1.23 +        Drule.implies_intr_list assms #>
    1.24 +        Drule.forall_intr_list fixes #>
    1.25 +        Thm.generalize (map #1 tfrees, []) 0);
    1.26      val local_result =
    1.27        Thm.future global_result (cert global_prop)
    1.28        |> Thm.instantiate (instT, [])
    1.29 @@ -178,7 +178,7 @@
    1.30            end);
    1.31      val res =
    1.32        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
    1.33 -      else future_result ctxt' result (Thm.term_of stmt);
    1.34 +      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
    1.35    in
    1.36      Conjunction.elim_balanced (length props) res
    1.37      |> map (Assumption.export false ctxt' ctxt)