# HG changeset patch
# User wenzelm
# Date 1333552459 -7200
# Node ID bd24e466bef9a37595057ec08a74c1b46f426980
# Parent  bed4b2738d8a01e112a7f2058323321001d9884b
tuned comments;

diff -r bed4b2738d8a -r bd24e466bef9 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Apr 04 14:19:47 2012 +0200
+++ b/src/Pure/global_theory.ML	Wed Apr 04 17:14:19 2012 +0200
@@ -49,7 +49,7 @@
 
 (** theory data **)
 
-type proofs = thm list * unit lazy;
+type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
 
 val empty_proofs: proofs = ([], Lazy.value ());
 
@@ -61,7 +61,7 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * (proofs * proofs);
+  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);