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