--- 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;