# HG changeset patch
# User wenzelm
# Date 1214229663 -7200
# Node ID efd626efcb0482f2bbe202ca0c72999bb3187d03
# Parent  d3beec3709646591aa1b122987a926cc161bb3c8
info: default name is "", not "Pure";

diff -r d3beec370964 -r efd626efcb04 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jun 23 15:51:38 2008 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jun 23 16:01:03 2008 +0200
@@ -82,9 +82,12 @@
   fun merge _ _ = empty;
 );
 
+val put_info = BrowserInfoData.put;
 val get_info = BrowserInfoData.get;
 val session_name = #name o get_info;
 
+val _ = Context.>> (Context.map_theory (put_info {name = "", session = [], is_local = false}));
+
 
 
 (** graphs **)
@@ -493,7 +496,7 @@
     add_graph_entry (update_time, entry);
     add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (update_time, Latex.theory_entry name);
-    BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
+    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
   end);