src/Pure/Thy/present.ML
changeset 33522 737589bb9bb8
parent 32738 15bb09ca0378
child 33682 0c5d1485dea7
     1.1 --- a/src/Pure/Thy/present.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -64,13 +64,12 @@
     1.4  
     1.5  (** additional theory data **)
     1.6  
     1.7 -structure BrowserInfoData = TheoryDataFun
     1.8 +structure BrowserInfoData = Theory_Data
     1.9  (
    1.10    type T = {name: string, session: string list, is_local: bool};
    1.11    val empty = {name = "", session = [], is_local = false}: T;
    1.12 -  val copy = I;
    1.13    fun extend _ = empty;
    1.14 -  fun merge _ _ = empty;
    1.15 +  fun merge _ = empty;
    1.16  );
    1.17  
    1.18  val put_info = BrowserInfoData.put;