src/Pure/global_theory.ML
changeset 44304 7ee000ce5390
parent 42471 593289343c7d
child 45643 9e49cfe7015d
     1.1 --- a/src/Pure/global_theory.ML	Fri Aug 19 21:40:52 2011 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Fri Aug 19 23:25:47 2011 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4    val intern_fact: theory -> xstring -> string
     1.5    val defined_fact: theory -> string -> bool
     1.6    val hide_fact: bool -> string -> theory -> theory
     1.7 +  val begin_recent_proofs: theory -> theory
     1.8 +  val join_recent_proofs: theory -> unit
     1.9    val join_proofs: theory -> unit
    1.10    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    1.11    val get_thms: theory -> xstring -> thm list
    1.12 @@ -49,10 +51,10 @@
    1.13  
    1.14  structure Data = Theory_Data
    1.15  (
    1.16 -  type T = Facts.T * thm list;
    1.17 -  val empty = (Facts.empty, []);
    1.18 -  fun extend (facts, _) = (facts, []);
    1.19 -  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
    1.20 +  type T = Facts.T * (thm list * thm list);
    1.21 +  val empty = (Facts.empty, ([], []));
    1.22 +  fun extend (facts, _) = (facts, ([], []));
    1.23 +  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
    1.24  );
    1.25  
    1.26  
    1.27 @@ -68,10 +70,11 @@
    1.28  
    1.29  (* proofs *)
    1.30  
    1.31 -fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
    1.32 +fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
    1.33  
    1.34 -fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
    1.35 -
    1.36 +val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
    1.37 +val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
    1.38 +val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
    1.39  
    1.40  
    1.41  (** retrieve theorems **)