# HG changeset patch
# User wenzelm
# Date 1346337590 -7200
# Node ID 72808e95687998470054404ef017c53bf69502d2
# Parent  15381ea111ecefa2505ead1275c03476eb74a1fb
tuned signature;

diff -r 15381ea111ec -r 72808e956879 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 16:39:50 2012 +0200
@@ -426,11 +426,11 @@
 
 val global_theory_group =
   Sign.new_group #>
-  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+  Thm.begin_recent_proofs #> Theory.checkpoint;
 
 val local_theory_group =
   Local_Theory.new_group #>
-  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+  Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
 
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
diff -r 15381ea111ec -r 72808e956879 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 30 16:39:50 2012 +0200
@@ -357,7 +357,7 @@
   is_some (Exn.get_res (Exn.capture (fn () =>
     fst (fst (Command.memo_result (the (get_result node))))
     |> Toplevel.end_theory Position.none
-    |> Global_Theory.join_proofs) ()));
+    |> Thm.join_all_proofs) ()));
 
 fun stable_command exec =
   (case Exn.capture Command.memo_result exec of
@@ -365,7 +365,7 @@
   | Exn.Res ((st, _), _) =>
       (case try Toplevel.theory_of st of
         NONE => true
-      | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
+      | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
 
 fun make_required nodes =
   let
diff -r 15381ea111ec -r 72808e956879 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 30 16:39:50 2012 +0200
@@ -176,7 +176,7 @@
 local
 
 fun finish_thy ((thy, present, commit): result) =
-  (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
+  (Thm.join_all_proofs thy; Future.join present; commit (); thy);
 
 val schedule_seq =
   Graph.schedule (fn deps => fn (_, task) =>
diff -r 15381ea111ec -r 72808e956879 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/global_theory.ML	Thu Aug 30 16:39:50 2012 +0200
@@ -10,9 +10,6 @@
   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
   val get_thm: theory -> xstring -> thm
@@ -49,42 +46,20 @@
 
 (** theory data **)
 
-type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
-
-val empty_proofs: proofs = ([], Lazy.value ());
-
-fun add_proofs more_thms ((thms, _): proofs) =
-  let val thms' = fold cons more_thms thms
-  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
-
-fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
-
 structure Data = Theory_Data
 (
-  type T = Facts.T * (proofs * proofs);  (*facts, recent proofs, all proofs of theory node*)
-  val empty = (Facts.empty, (empty_proofs, empty_proofs));
-  fun extend (facts, _) = (facts, snd empty);
-  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty);
+  type T = Facts.T;
+  val empty = Facts.empty;
+  val extend = I;
+  val merge = Facts.merge;
 );
 
-
-(* facts *)
-
-val facts_of = #1 o Data.get;
+val facts_of = Data.get;
 
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;
 
-fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
-
-
-(* forked proofs *)
-
-fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
-
-val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
-val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
-val join_proofs = force_proofs o #2 o #2 o Data.get;
+fun hide_fact fully name = Data.map (Facts.hide fully name);
 
 
 (** retrieve theorems **)
@@ -149,6 +124,8 @@
 
 (* enter_thms *)
 
+fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
+
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
   then app_att thms thy |-> register_proofs
@@ -157,8 +134,7 @@
       val name = Sign.full_name thy b;
       val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
       val thms'' = map (Thm.transfer thy') thms';
-      val thy'' = thy'
-        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
+      val thy'' = thy' |> Data.map (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
     in (thms'', thy'') end;
 
 
@@ -192,7 +168,7 @@
 (* add_thms_dynamic *)
 
 fun add_thms_dynamic (b, f) thy = thy
-  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
+  |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
 
 
 (* note_thmss *)
diff -r 15381ea111ec -r 72808e956879 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Aug 30 15:26:37 2012 +0200
+++ b/src/Pure/more_thm.ML	Thu Aug 30 16:39:50 2012 +0200
@@ -95,6 +95,10 @@
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
+  val register_proofs: thm list -> theory -> theory
+  val begin_recent_proofs: theory -> theory
+  val join_recent_proofs: theory -> unit
+  val join_all_proofs: theory -> unit
 end;
 
 structure Thm: THM =
@@ -466,6 +470,33 @@
 fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
 
 
+(* forked proofs within the context *)
+
+type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
+
+val empty_proofs: proofs = ([], Lazy.value ());
+
+fun add_proofs more_thms ((thms, _): proofs) =
+  let val thms' = fold cons more_thms thms
+  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
+
+fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
+
+structure Proofs = Theory_Data
+(
+  type T = proofs * proofs;  (*recent proofs, all proofs of theory node*)
+  val empty = (empty_proofs, empty_proofs);
+  fun extend _ = empty;
+  fun merge _ = empty;
+);
+
+val register_proofs = Proofs.map o pairself o add_proofs;
+val begin_recent_proofs = Proofs.map (apfst (K empty_proofs));
+
+val join_recent_proofs = force_proofs o #1 o Proofs.get;
+val join_all_proofs = force_proofs o #2 o Proofs.get;
+
+
 open Thm;
 
 end;