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