diff -r e936d3c35ce0 -r 2ba492b8b6e8 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Jan 04 22:43:07 2010 +0100
+++ b/src/Pure/context.ML	Mon Jan 04 23:20:35 2010 +0100
@@ -574,7 +574,7 @@
 
 (** theory data **)
 
-signature OLD_THEORY_DATA_ARGS =
+signature THEORY_DATA_PP_ARGS =
 sig
   type T
   val empty: T
@@ -582,6 +582,14 @@
   val merge: Pretty.pp -> T * T -> T
 end;
 
+signature THEORY_DATA_ARGS =
+sig
+  type T
+  val empty: T
+  val extend: T -> T
+  val merge: T * T -> T
+end;
+
 signature THEORY_DATA =
 sig
   type T
@@ -590,7 +598,7 @@
   val map: (T -> T) -> theory -> theory
 end;
 
-functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
+functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -607,28 +615,14 @@
 
 end;
 
-signature THEORY_DATA_ARGS =
-sig
-  type T
-  val empty: T
-  val extend: T -> T
-  val merge: T * T -> T
-end;
-
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
-struct
-
-structure Result = TheoryDataFun
-(
-  type T = Data.T;
-  val empty = Data.empty;
-  val extend = Data.extend;
-  fun merge _ = Data.merge;
-);
-
-open Result;
-
-end;
+  Theory_Data_PP
+  (
+    type T = Data.T;
+    val empty = Data.empty;
+    val extend = Data.extend;
+    fun merge _ = Data.merge;
+  );