# HG changeset patch
# User haftmann
# Date 1231363984 -3600
# Node ID 4638ab6c878f80507cbe61028b67680b60f97726
# Parent  d23fdfa46b6a3d18eb6d699ed536357528727c1a# Parent  172213e44992099dbd9493b37a7671667c05b8a0
merged

diff -r 172213e44992 -r 4638ab6c878f src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -199,14 +199,14 @@
 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
 
 val by_pat_completeness_simp =
-    Proof.future_terminal_proof
+    Proof.global_future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
-fun termination_by method =
+fun termination_by method int =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.future_terminal_proof
-      (Method.Basic (method, Position.none), NONE)
+    #> Proof.global_future_terminal_proof
+      (Method.Basic (method, Position.none), NONE) int
 
 fun mk_catchall fixes arities =
     let
@@ -304,19 +304,19 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-fun fun_cmd config fixes statements flags lthy =
+fun fun_cmd config fixes statements flags int lthy =
   let val group = serial_string () in
     lthy
       |> LocalTheory.set_group group
       |> FundefPackage.add_fundef fixes statements config flags
-      |> by_pat_completeness_simp
+      |> by_pat_completeness_simp int
       |> LocalTheory.restore
       |> LocalTheory.set_group group
-      |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy))
+      |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int
   end;
 
 val _ =
-  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+  OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
      >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags));
 
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -145,8 +145,9 @@
 fun execute name (task, group, jobs) =
   let
     val _ = trace_active ();
+    val valid = Task_Queue.is_valid group;
     val ok = setmp_thread_data (name, task) (fn () =>
-      fold (fn job => fn ok => job ok) jobs (Task_Queue.is_valid group)) ();
+      fold (fn job => fn ok => job valid andalso ok) jobs true) ();
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (Task_Queue.finish task);
       if ok then ()
@@ -311,18 +312,21 @@
 
 (* map *)
 
-fun map_future f (x as Future {task, group, ...}) =
+fun map_future f x =
   let
     val _ = scheduler_check "map_future check";
 
-    val (result', job) = future_job group (fn () => f (join x));
+    val task = task_of x;
+    val group = Task_Queue.new_group ();
+    val (result, job) = future_job group (fn () => f (join x));
+
     val extended = SYNCHRONIZED "map_future" (fn () =>
       (case Task_Queue.extend task job (! queue) of
         SOME queue' => (queue := queue'; true)
       | NONE => false));
   in
-    if extended then Future {task = task, group = group, result = result'}
-    else fork_future (SOME group) [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
+    if extended then Future {task = task, group = group, result = result}
+    else fork_future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
   end;
 
 
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -889,7 +889,7 @@
       end;
 
     fun after_qed results =
-      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
+      Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
   in
     state |> Proof.map_context (K goal_ctxt) |>
       Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Derived Isar commands.
@@ -219,7 +218,7 @@
 (* goals *)
 
 fun goal opt_chain goal stmt int =
-  opt_chain #> goal NONE (K Seq.single) stmt int;
+  opt_chain #> goal NONE (K I) stmt int;
 
 val have = goal I Proof.have;
 val hence = goal Proof.chain Proof.have;
@@ -229,12 +228,12 @@
 
 (* local endings *)
 
-fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
-val local_default_proof = Toplevel.proofs Proof.local_default_proof;
-val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
-val local_done_proof = Toplevel.proofs Proof.local_done_proof;
-val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
+fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
+val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_default_proof = Toplevel.proof Proof.local_default_proof;
+val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
+val local_done_proof = Toplevel.proof Proof.local_done_proof;
+val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
 
 val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
 
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/obtain.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The 'obtain' and 'guess' language elements -- generalized existence at
@@ -150,13 +149,13 @@
 
     fun after_qed _ =
       Proof.local_qed (NONE, false)
-      #> Seq.map (`Proof.the_fact #-> (fn rule =>
+      #> `Proof.the_fact #-> (fn rule =>
         Proof.fix_i vars
-        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
+        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
@@ -306,7 +305,7 @@
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
-      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
+      Proof.end_block #> guess_context (check_result ctxt thesis res);
   in
     state
     |> Proof.enter_forward
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/old_locale.ML
--- a/src/Pure/Isar/old_locale.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/old_locale.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -116,7 +116,7 @@
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
-  val interpret: (Proof.state -> Proof.state Seq.seq) ->
+  val interpret: (Proof.state -> Proof.state) ->
     (Binding.T -> Binding.T) -> expr ->
     term option list * (Attrib.binding * term) list ->
     bool -> Proof.state ->
@@ -2478,7 +2478,7 @@
 
 val interpret = gen_interpret prep_local_registration;
 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
-  Seq.single (standard_name_morph interp_prfx);
+  I (standard_name_morph interp_prfx);
 
 end;
 
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -17,6 +17,8 @@
   val improper_command: string -> string -> OuterKeyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val local_theory': string -> string -> OuterKeyword.T ->
+    (bool -> local_theory -> local_theory) parser -> unit
   val local_theory: string -> string -> OuterKeyword.T ->
     (local_theory -> local_theory) parser -> unit
   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
@@ -138,6 +140,7 @@
   command name comment kind (P.opt_target -- parse
     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
 
+val local_theory' = local_theory_command false Toplevel.local_theory';
 val local_theory = local_theory_command false Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -30,7 +30,6 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val get_goal: state -> context * (thm list * thm)
-  val schematic_goal: state -> bool
   val show_main_goal: bool ref
   val verbose: bool ref
   val pretty_state: int -> state -> Pretty.T list
@@ -87,35 +86,40 @@
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
+    string -> Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * 'a list) * 'b) list -> state -> state
-  val local_qed: Method.text option * bool -> state -> state Seq.seq
+  val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
   val theorem_i: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
-  val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
-  val local_default_proof: state -> state Seq.seq
-  val local_immediate_proof: state -> state Seq.seq
-  val local_done_proof: state -> state Seq.seq
-  val local_skip_proof: bool -> state -> state Seq.seq
+  val local_terminal_proof: Method.text * Method.text option -> state -> state
+  val local_default_proof: state -> state
+  val local_immediate_proof: state -> state
+  val local_skip_proof: bool -> state -> state
+  val local_done_proof: state -> state
   val global_terminal_proof: Method.text * Method.text option -> state -> context
   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
+  val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
-  val global_skip_proof: bool -> state -> context
-  val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
-  val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+  val schematic_goal: state -> bool
   val is_relevant: state -> bool
-  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val future_terminal_proof: Method.text * Method.text option -> state -> context
+  val local_future_proof: (state -> ('a * state) Future.future) ->
+    state -> 'a Future.future * state
+  val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
+    state -> 'a Future.future * context
+  val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
+  val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -148,7 +152,7 @@
     goal: thm,                            (*subgoals ==> statement*)
     before_qed: Method.text option,
     after_qed:
-      (thm list list -> state -> state Seq.seq) *
+      (thm list list -> state -> state) *
       (thm list list -> context -> context)};
 
 fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
@@ -312,12 +316,6 @@
   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   in (ctxt, (using, goal)) end;
 
-fun schematic_goal state =
-  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state in
-    Term.exists_subterm Term.is_Var prop orelse
-    Term.exists_type (Term.exists_subtype Term.is_TVar) prop
-  end;
-
 
 
 (** pretty_state **)
@@ -347,8 +345,7 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i,
-            {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
@@ -751,6 +748,13 @@
   |> `before_qed |-> (refine o the_default Method.succeed_text)
   |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
 
+fun check_result msg sq =
+  (case Seq.pull sq of
+    NONE => error msg
+  | SOME (s, _) => s);
+
+fun check_finish sq = check_result "Failed to finish proof" sq;
+
 
 (* unstructured refinement *)
 
@@ -842,7 +846,7 @@
       |> burrow (ProofContext.export goal_ctxt outer_ctxt);
 
     val (after_local, after_global) = after_qed;
-    fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
+    fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
     fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   in
     outer_state
@@ -871,61 +875,47 @@
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
-fun local_qed txt =
-  end_proof false txt #>
-  Seq.maps (generic_qed ProofContext.auto_bind_facts #->
+fun local_qeds txt =
+  end_proof false txt
+  #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
     (fn ((after_qed, _), results) => after_qed results));
 
+fun local_qed txt = local_qeds txt #> check_finish;
+
 
 (* global goals *)
 
 fun global_goal prepp before_qed after_qed propp ctxt =
   init ctxt
-  |> generic_goal (prepp #> ProofContext.auto_fixes) ""
-    before_qed (K Seq.single, after_qed) propp;
+  |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
 
 val theorem = global_goal ProofContext.bind_propp_schematic;
 val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
 
-fun check_result msg sq =
-  (case Seq.pull sq of
-    NONE => error msg
-  | SOME (s', sq') => Seq.cons s' sq');
-
 fun global_qeds txt =
   end_proof true txt
   #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state)))
-  |> Seq.DETERM;   (*backtracking may destroy theory!*)
+    after_qed results (context_of state)));
 
-fun global_qed txt =
-  global_qeds txt
-  #> check_result "Failed to finish proof"
-  #> Seq.hd;
+fun global_qed txt = global_qeds txt #> check_finish;
 
 
 (* concluding steps *)
 
-fun local_terminal_proof (text, opt_text) =
-  proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
+fun terminal_proof qed initial terminal =
+  proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
 
+fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
 val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
-val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
 fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
+val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
 
-fun global_term_proof immed (text, opt_text) =
-  proof (SOME text)
-  #> check_result "Terminal proof method failed"
-  #> Seq.maps (global_qeds (opt_text, immed))
-  #> check_result "Failed to finish proof (after successful terminal method)"
-  #> Seq.hd;
-
-val global_terminal_proof = global_term_proof true;
+fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
 val global_default_proof = global_terminal_proof (Method.default_text, NONE);
 val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
-val global_done_proof = global_term_proof false (Method.done_text, NONE);
 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
+val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
 
 
 (* common goal statements *)
@@ -940,7 +930,7 @@
     val testing = ref false;
     val rule = ref (NONE: thm option);
     fun fail_msg ctxt =
-      "Local statement will fail to solve any pending goal" ::
+      "Local statement will fail to refine any pending goal" ::
       (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
@@ -951,13 +941,14 @@
       else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
-      (Seq.pull oo local_skip_proof) true
+      try (local_skip_proof true)
       |> setmp_noncritical testing true
       |> Exn.capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
-      #> Seq.maps (after_qed results);
+      #> check_result "Failed to refine any pending goal"
+      #> after_qed results;
   in
     state
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
@@ -979,59 +970,89 @@
 end;
 
 
-(* fork global proofs *)
+
+(** future proofs **)
+
+(* relevant proof states *)
+
+fun is_schematic t =
+  Term.exists_subterm Term.is_Var t orelse
+  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
+
+fun schematic_goal state =
+  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
+  in is_schematic prop end;
+
+fun is_relevant state =
+  (case try find_goal state of
+    NONE => true
+  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
+      is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+
+
+(* full proofs *)
 
 local
 
-fun is_original state =
-  (case try find_goal state of
-    NONE => false
-  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
-      Logic.protect prop aconv Thm.concl_of goal);
-
-in
-
-fun is_relevant state =
-  can (assert_bottom false) state orelse
-  can assert_forward state orelse
-  not (is_original state) orelse
-  schematic_goal state;
-
-fun future_proof fork_proof state =
+fun future_proof done get_context fork_proof state =
   let
-    val _ = is_relevant state andalso error "Cannot fork relevant proof";
-
+    val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
 
+    val _ = is_relevant state andalso error "Cannot fork relevant proof";
+
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');
     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
       (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
-    fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+
+    fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
+    fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+    val after_qed' = (after_local', after_global');
     val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
 
     val result_ctxt =
       state
-      |> map_contexts (Variable.auto_fixes prop)
-      |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
+      |> map_contexts (Variable.declare_term prop)
+      |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
       |> fork_proof;
 
-    val future_thm = result_ctxt |> Future.map (fn (_, ctxt) =>
-      ProofContext.get_fact_single ctxt (Facts.named this_name));
-    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+    val future_thm = result_ctxt |> Future.map (fn (_, x) =>
+      ProofContext.get_fact_single (get_context x) (Facts.named this_name));
+    val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
     val state' =
       state
       |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
-      |> global_done_proof;
+      |> done;
   in (Future.map #1 result_ctxt, state') end;
 
+in
+
+fun local_future_proof x = future_proof local_done_proof context_of x;
+fun global_future_proof x = future_proof global_done_proof I x;
+
 end;
 
-fun future_terminal_proof meths state =
-  if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
-  else #2 (state |> future_proof (fn state' =>
-    Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+
+(* terminal proofs *)
+
+local
+
+fun future_terminal_proof proof1 proof2 meths int state =
+  if int orelse is_relevant state orelse not (Future.enabled ())
+  then proof1 meths state
+  else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+
+in
+
+fun local_future_terminal_proof x =
+  future_terminal_proof local_terminal_proof local_future_proof x;
+
+fun global_future_terminal_proof x =
+  future_terminal_proof global_terminal_proof global_future_proof x;
 
 end;
 
+end;
+
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/toplevel.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Isabelle/Isar toplevel transactions.
@@ -66,6 +65,8 @@
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
+  val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
+    transition -> transition
   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
   val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
@@ -512,14 +513,15 @@
   (fn Theory (gthy, _) =>
         let
           val finish = loc_finish loc gthy;
-          val lthy' = f (loc_begin loc gthy);
+          val lthy' = f int (loc_begin loc gthy);
         in Theory (finish lthy', SOME lthy') end
     | _ => raise UNDEF) #> tap g);
 
 in
 
-fun local_theory loc f = local_theory_presentation loc f (K I);
-fun present_local_theory loc g = local_theory_presentation loc I g;
+fun local_theory' loc f = local_theory_presentation loc f (K I);
+fun local_theory loc f = local_theory' loc (K f);
+fun present_local_theory loc g = local_theory_presentation loc (K I) g;
 
 end;
 
@@ -716,7 +718,7 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o ProofContext.theory_of;
 
-        val future_proof = Proof.future_proof
+        val future_proof = Proof.global_future_proof
           (fn prf =>
             Future.fork_pri ~1 (fn () =>
               let val (states, State (result_node, _)) =
diff -r 172213e44992 -r 4638ab6c878f src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Wed Jan 07 22:31:37 2009 +0100
+++ b/src/Pure/Tools/invoke.ML	Wed Jan 07 22:33:04 2009 +0100
@@ -88,7 +88,7 @@
           |> (snd o ProofContext.note_thmss_i "" notes)
           |> ProofContext.restore_naming ctxt
         end) #>
-      Proof.put_facts NONE #> Seq.single;
+      Proof.put_facts NONE;
   in
     state'
     |> Proof.chain_facts chain_facts