discontinued complicated/unreliable notion of recent proofs within context;

--- a/src/Pure/Isar/local_theory.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -30,8 +30,6 @@
   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
@@ -192,12 +190,6 @@
 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 Thm.register_proofs_thy;
-
-
 (* target contexts *)
 
 val target_of = #target o get_last_lthy;

--- a/src/Pure/Isar/proof.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -21,9 +21,6 @@
   val propagate_ml_env: state -> state
   val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
-  val begin_proofs: state -> state
-  val register_proofs: thm list -> state -> state
-  val join_recent_proofs: state -> unit
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val set_facts: thm list -> state -> state
@@ -225,14 +222,6 @@
 val put_thms = map_context oo Proof_Context.put_thms;
 
 
-(* forked proofs *)
-
-val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
-val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
-
-val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
-
-
 (* facts *)
 
 val get_facts = #facts o top;
@@ -966,7 +955,7 @@
 fun local_qeds txt =
   end_proof false txt
   #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results));
+    (fn ((after_qed, _), results) => after_qed results));
 
 fun local_qed txt = local_qeds txt #> check_finish;
 

--- a/src/Pure/Isar/specification.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -395,8 +395,7 @@
       let
         val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
         val (res, lthy') =
-          if forall (Attrib.is_empty_binding o fst) stmt
-          then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy)
+          if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
           else
             Local_Theory.notes_kind kind
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;

--- a/src/Pure/Isar/toplevel.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -53,7 +53,6 @@
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val is_malformed: transition -> bool
-  val join_recent_proofs: state -> unit
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
@@ -423,21 +422,6 @@
 val unknown_context = imperative (fn () => warning "Unknown context");
 
 
-(* forked proofs *)
-
-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
-    SOME prf => Proof.join_recent_proofs prf
-  | NONE =>
-      (case try theory_of st of
-        SOME thy => Thm.join_recent_proofs thy
-      | NONE => ()));
-
-
 (* theory transitions *)
 
 fun generic_theory f = transaction (fn _ =>
@@ -487,9 +471,7 @@
 fun local_theory_presentation loc f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
-          val (finish, lthy) = gthy
-            |> begin_proofs
-            |> loc_begin loc;
+          val (finish, lthy) = loc_begin loc gthy;
           val lthy' = lthy
             |> Local_Theory.new_group
             |> f int
@@ -545,9 +527,7 @@
 
 fun local_theory_to_proof' loc f = begin_proof
   (fn int => fn gthy =>
-    let val (finish, lthy) = gthy
-      |> begin_proofs
-      |> loc_begin loc;
+    let val (finish, lthy) = loc_begin loc gthy
     in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
@@ -555,7 +535,7 @@
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
     (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
-      (case begin_proofs gthy of
+      (case gthy of
         Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
       | _ => raise UNDEF)));
 
@@ -567,12 +547,12 @@
     | _ => raise UNDEF));
 
 val present_proof = present_transaction (fn _ =>
-  (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 
 fun proofs' f = transaction (fn int =>
-  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
+  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
 

--- a/src/Pure/global_theory.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/global_theory.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -124,7 +124,7 @@
 
 (* enter_thms *)
 
-fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy);
+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

--- a/src/Pure/more_thm.ML	Sat Sep 01 19:27:28 2012 +0200
+++ b/src/Pure/more_thm.ML	Sat Sep 01 19:43:18 2012 +0200
@@ -95,11 +95,7 @@
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
-  val register_proofs: thm list -> Context.generic -> Context.generic
-  val register_proofs_thy: thm list -> theory -> theory
-  val begin_proofs: Context.generic -> Context.generic
-  val join_local_proofs: Proof.context -> unit
-  val join_recent_proofs: theory -> unit
+  val register_proofs: thm list -> theory -> theory
   val join_theory_proofs: theory -> unit
 end;
 
@@ -474,31 +470,16 @@
 
 (* forked proofs *)
 
-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 = Generic_Data
+structure Proofs = Theory_Data
 (
-  type T = proofs * proofs;  (*recent proofs since last begin, all proofs of theory node*)
-  val empty = (empty_proofs, empty_proofs);
+  type T = thm list;
+  val empty = [];
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
-val begin_proofs = Proofs.map (apfst (K empty_proofs));
-val register_proofs = Proofs.map o pairself o add_proofs;
-val register_proofs_thy = Context.theory_map o register_proofs;
-
-val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
-val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
-val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
+fun register_proofs more_thms = Proofs.map (fn thms => fold cons more_thms thms);
+val join_theory_proofs = Thm.join_proofs o rev o Proofs.get;
 
 
 open Thm;