1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Aug 19 21:40:52 2011 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Aug 19 23:25:47 2011 +0200
     1.3 @@ -419,6 +419,14 @@
     1.4  
     1.5  (* theory transitions *)
     1.6  
     1.7 +val global_theory_group =
     1.8 +  Sign.new_group #>
     1.9 +  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
    1.10 +
    1.11 +val local_theory_group =
    1.12 +  Local_Theory.new_group #>
    1.13 +  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
    1.14 +
    1.15  fun generic_theory f = transaction (fn _ =>
    1.16    (fn Theory (gthy, _) => Theory (f gthy, NONE)
    1.17      | _ => raise UNDEF));
    1.18 @@ -426,8 +434,7 @@
    1.19  fun theory' f = transaction (fn int =>
    1.20    (fn Theory (Context.Theory thy, _) =>
    1.21        let val thy' = thy
    1.22 -        |> Sign.new_group
    1.23 -        |> Theory.checkpoint
    1.24 +        |> global_theory_group
    1.25          |> f int
    1.26          |> Sign.reset_group;
    1.27        in Theory (Context.Theory thy', NONE) end
    1.28 @@ -454,7 +461,7 @@
    1.29          let
    1.30            val finish = loc_finish loc gthy;
    1.31            val lthy' = loc_begin loc gthy
    1.32 -            |> Local_Theory.new_group
    1.33 +            |> local_theory_group
    1.34              |> f int
    1.35              |> Local_Theory.reset_group;
    1.36          in Theory (finish lthy', SOME lthy') end
    1.37 @@ -506,13 +513,13 @@
    1.38  in
    1.39  
    1.40  fun local_theory_to_proof' loc f = begin_proof
    1.41 -  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
    1.42 +  (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
    1.43    (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
    1.44  
    1.45  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    1.46  
    1.47  fun theory_to_proof f = begin_proof
    1.48 -  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
    1.49 +  (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
    1.50    (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
    1.51  
    1.52  end;

     2.1 --- a/src/Pure/global_theory.ML	Fri Aug 19 21:40:52 2011 +0200
     2.2 +++ b/src/Pure/global_theory.ML	Fri Aug 19 23:25:47 2011 +0200
     2.3 @@ -10,6 +10,8 @@
     2.4    val intern_fact: theory -> xstring -> string
     2.5    val defined_fact: theory -> string -> bool
     2.6    val hide_fact: bool -> string -> theory -> theory
     2.7 +  val begin_recent_proofs: theory -> theory
     2.8 +  val join_recent_proofs: theory -> unit
     2.9    val join_proofs: theory -> unit
    2.10    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    2.11    val get_thms: theory -> xstring -> thm list
    2.12 @@ -49,10 +51,10 @@
    2.13  
    2.14  structure Data = Theory_Data
    2.15  (
    2.16 -  type T = Facts.T * thm list;
    2.17 -  val empty = (Facts.empty, []);
    2.18 -  fun extend (facts, _) = (facts, []);
    2.19 -  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
    2.20 +  type T = Facts.T * (thm list * thm list);
    2.21 +  val empty = (Facts.empty, ([], []));
    2.22 +  fun extend (facts, _) = (facts, ([], []));
    2.23 +  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
    2.24  );
    2.25  
    2.26  
    2.27 @@ -68,10 +70,11 @@
    2.28  
    2.29  (* proofs *)
    2.30  
    2.31 -fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
    2.32 +fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
    2.33  
    2.34 -fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
    2.35 -
    2.36 +val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
    2.37 +val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
    2.38 +val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
    2.39  
    2.40  
    2.41  (** retrieve theorems **)