more precise register_proofs for local goals;
tuned signature;

--- a/src/Pure/Isar/local_theory.ML	Fri Aug 31 15:25:26 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 31 16:35:30 2012 +0200
@@ -30,6 +30,8 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
+  val begin_proofs: local_theory -> local_theory
+  val register_proofs: thm list -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
@@ -190,6 +192,12 @@
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
 
+(* forked proofs *)
+
+val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs);
+val register_proofs = background_theory o Context.theory_map o Thm.register_proofs;
+
+
 (* target contexts *)
 
 val target_of = #target o get_last_lthy;

--- a/src/Pure/Isar/proof.ML	Fri Aug 31 15:25:26 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Aug 31 16:35:30 2012 +0200
@@ -78,15 +78,15 @@
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
-  val begin_notepad: Proof.context -> state
-  val end_notepad: state -> Proof.context
+  val begin_notepad: context -> state
+  val end_notepad: state -> context
   val proof: Method.text option -> state -> state Seq.seq
   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
-    (Proof.context -> 'a -> attribute) ->
+    (context -> 'a -> attribute) ->
     ('b list -> context -> (term list list * (context -> context)) * context) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
@@ -116,7 +116,7 @@
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
-  val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
+  val global_future_proof: (state -> ('a * context) future) -> state -> 'a 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;
@@ -939,7 +939,6 @@
       |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
   in
     outer_state
-    |> register_proofs (flat results)
     |> map_context (after_ctxt props)
     |> pair (after_qed, results)
   end;
@@ -967,7 +966,7 @@
 fun local_qeds txt =
   end_proof false txt
   #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results));
+    (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results));
 
 fun local_qed txt = local_qeds txt #> check_finish;
 

--- a/src/Pure/Isar/toplevel.ML	Fri Aug 31 15:25:26 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Aug 31 16:35:30 2012 +0200
@@ -425,8 +425,9 @@
 
 (* forked proofs *)
 
-val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
-val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
+val begin_proofs =
+  Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint)
+    Local_Theory.begin_proofs;
 
 fun join_recent_proofs st =
   (case try proof_of st of