# HG changeset patch
# User wenzelm
# Date 1119298458 -7200
# Node ID 24491bde68dffac546ce408b0cfee0477041ccf7
# Parent  5a56e59526a5069d126aaaf53a21deb075862cda
clarify empty vs. pure browser info;

diff -r 5a56e59526a5 -r 24491bde68df src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jun 20 22:14:17 2005 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jun 20 22:14:18 2005 +0200
@@ -72,15 +72,13 @@
 
 (** additional theory data **)
 
-val empty_browser_info = {name = "Pure", session = []: string list, is_local = false};
-
 structure BrowserInfoData = TheoryDataFun
 (struct
   val name = "Pure/browser_info";
   type T = {name: string, session: string list, is_local: bool};
-  val empty = empty_browser_info;
+  val empty = {name = "", session = [], is_local = false}: T;
   val copy = I;
-  fun extend _ = {name = "", session = [], is_local = false};
+  fun extend _ = empty;
   fun merge _ _ = empty;
   fun print _ _ = ();
 end);
@@ -89,7 +87,7 @@
 
 fun get_info thy =
   if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
-  then empty_browser_info
+  then {name = Context.PureN, session = [], is_local = false}
   else BrowserInfoData.get thy;