1.1 --- a/src/Pure/Thy/present.ML	Mon Jun 20 22:14:17 2005 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Jun 20 22:14:18 2005 +0200
     1.3 @@ -72,15 +72,13 @@
     1.4  
     1.5  (** additional theory data **)
     1.6  
     1.7 -val empty_browser_info = {name = "Pure", session = []: string list, is_local = false};
     1.8 -
     1.9  structure BrowserInfoData = TheoryDataFun
    1.10  (struct
    1.11    val name = "Pure/browser_info";
    1.12    type T = {name: string, session: string list, is_local: bool};
    1.13 -  val empty = empty_browser_info;
    1.14 +  val empty = {name = "", session = [], is_local = false}: T;
    1.15    val copy = I;
    1.16 -  fun extend _ = {name = "", session = [], is_local = false};
    1.17 +  fun extend _ = empty;
    1.18    fun merge _ _ = empty;
    1.19    fun print _ _ = ();
    1.20  end);
    1.21 @@ -89,7 +87,7 @@
    1.22  
    1.23  fun get_info thy =
    1.24    if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
    1.25 -  then empty_browser_info
    1.26 +  then {name = Context.PureN, session = [], is_local = false}
    1.27    else BrowserInfoData.get thy;
    1.28  
    1.29