1.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 04 23:00:27 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 04 23:00:58 2008 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     1.5      ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
     1.6    val is_relevant: state -> bool
     1.7 -  val future_proof: (state -> context) -> state -> context
     1.8 +  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
     1.9  end;
    1.10  
    1.11  structure Proof: PROOF =
    1.12 @@ -990,7 +990,7 @@
    1.13    not (is_initial state) orelse
    1.14    schematic_goal state;
    1.15  
    1.16 -fun future_proof make_proof state =
    1.17 +fun future_proof proof state =
    1.18    let
    1.19      val _ = is_relevant state andalso error "Cannot fork relevant proof";
    1.20  
    1.21 @@ -1004,16 +1004,19 @@
    1.22      fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
    1.23      val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
    1.24  
    1.25 -    fun make_result () = state
    1.26 +    val result_ctxt =
    1.27 +      state
    1.28        |> map_contexts (Variable.auto_fixes prop)
    1.29        |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
    1.30 -      |> make_proof
    1.31 -      |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
    1.32 -    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
    1.33 -  in
    1.34 -    state
    1.35 -    |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
    1.36 -    |> global_done_proof
    1.37 -  end;
    1.38 +      |> proof;
    1.39 +
    1.40 +    val thm = result_ctxt |> Future.map (fn (_, ctxt) =>
    1.41 +      ProofContext.get_fact_single ctxt (Facts.named this_name));
    1.42 +    val finished_goal = Goal.protect (Goal.future_result goal_ctxt thm prop);
    1.43 +    val state' =
    1.44 +      state
    1.45 +      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
    1.46 +      |> global_done_proof;
    1.47 +  in (Future.map #1 result_ctxt, state') end;
    1.48  
    1.49  end;

     2.1 --- a/src/Pure/goal.ML	Thu Dec 04 23:00:27 2008 +0100
     2.2 +++ b/src/Pure/goal.ML	Thu Dec 04 23:00:58 2008 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4    val conclude: thm -> thm
     2.5    val finish: thm -> thm
     2.6    val norm_result: thm -> thm
     2.7 -  val future_result: Proof.context -> (unit -> thm) -> term -> thm
     2.8 +  val future_result: Proof.context -> thm future -> term -> thm
     2.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    2.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    2.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    2.12 @@ -116,11 +116,11 @@
    2.13  
    2.14      val global_prop =
    2.15        Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
    2.16 -    val global_result =
    2.17 -      Thm.generalize (map #1 tfrees, []) 0 o
    2.18 -      Drule.forall_intr_list fixes o
    2.19 -      Drule.implies_intr_list assms o
    2.20 -      Thm.adjust_maxidx_thm ~1 o result;
    2.21 +    val global_result = result |> Future.map
    2.22 +      (Thm.adjust_maxidx_thm ~1 #>
    2.23 +        Drule.implies_intr_list assms #>
    2.24 +        Drule.forall_intr_list fixes #>
    2.25 +        Thm.generalize (map #1 tfrees, []) 0);
    2.26      val local_result =
    2.27        Thm.future global_result (cert global_prop)
    2.28        |> Thm.instantiate (instT, [])
    2.29 @@ -178,7 +178,7 @@
    2.30            end);
    2.31      val res =
    2.32        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
    2.33 -      else future_result ctxt' result (Thm.term_of stmt);
    2.34 +      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
    2.35    in
    2.36      Conjunction.elim_balanced (length props) res
    2.37      |> map (Assumption.export false ctxt' ctxt)