maintain recent future proofs at transaction boundaries;

--- a/src/Pure/Isar/toplevel.ML	Fri Aug 19 21:40:52 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Aug 19 23:25:47 2011 +0200
@@ -419,6 +419,14 @@
 
 (* theory transitions *)
 
+val global_theory_group =
+  Sign.new_group #>
+  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+
+val local_theory_group =
+  Local_Theory.new_group #>
+  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
     | _ => raise UNDEF));
@@ -426,8 +434,7 @@
 fun theory' f = transaction (fn int =>
   (fn Theory (Context.Theory thy, _) =>
       let val thy' = thy
-        |> Sign.new_group
-        |> Theory.checkpoint
+        |> global_theory_group
         |> f int
         |> Sign.reset_group;
       in Theory (Context.Theory thy', NONE) end
@@ -454,7 +461,7 @@
         let
           val finish = loc_finish loc gthy;
           val lthy' = loc_begin loc gthy
-            |> Local_Theory.new_group
+            |> local_theory_group
             |> f int
             |> Local_Theory.reset_group;
         in Theory (finish lthy', SOME lthy') end
@@ -506,13 +513,13 @@
 in
 
 fun local_theory_to_proof' loc f = begin_proof
-  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+  (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
   (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
-  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+  (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
   (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
 
 end;

--- a/src/Pure/global_theory.ML	Fri Aug 19 21:40:52 2011 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 19 23:25:47 2011 +0200
@@ -10,6 +10,8 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
+  val begin_recent_proofs: theory -> theory
+  val join_recent_proofs: theory -> unit
   val join_proofs: theory -> unit
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
@@ -49,10 +51,10 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * thm list;
-  val empty = (Facts.empty, []);
-  fun extend (facts, _) = (facts, []);
-  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+  type T = Facts.T * (thm list * thm list);
+  val empty = (Facts.empty, ([], []));
+  fun extend (facts, _) = (facts, ([], []));
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
 );
 
 
@@ -68,10 +70,11 @@
 
 (* proofs *)
 
-fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
 
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
-
+val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
+val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
+val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
 
 
 (** retrieve theorems **)