diff -r b589bbbdb1b6 -r 5930c6391126 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Jan 04 19:44:46 2010 +0100
+++ b/src/Pure/context.ML	Mon Jan 04 20:25:56 2010 +0100
@@ -426,9 +426,9 @@
 val declare = declare_theory_data;
 
 fun get k dest thy =
-  dest (case Datatab.lookup (data_of thy) k of
+  (case Datatab.lookup (data_of thy) k of
     SOME x => x
-  | NONE => invoke_empty k);   (*adhoc value*)
+  | NONE => invoke_empty k) |> dest;
 
 fun put k mk x = modify_thy (Datatab.update (k, mk x));
 
@@ -582,16 +582,15 @@
   val merge: Pretty.pp -> T * T -> T
 end;
 
-signature OLD_THEORY_DATA =
+signature THEORY_DATA =
 sig
   type T
   val get: theory -> T
   val put: T -> theory -> theory
   val map: (T -> T) -> theory -> theory
-  val init: theory -> theory
 end;
 
-functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
+functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -606,8 +605,6 @@
 val put = Context.Theory_Data.put kind Data;
 fun map f thy = put (f (get thy)) thy;
 
-fun init thy = map I thy;
-
 end;
 
 signature THEORY_DATA_ARGS =
@@ -618,14 +615,6 @@
   val merge: T * T -> T
 end;
 
-signature THEORY_DATA =
-sig
-  type T
-  val get: theory -> T
-  val put: T -> theory -> theory
-  val map: (T -> T) -> theory -> theory
-end;
-
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
 struct