1.1 --- a/src/Pure/context.ML	Mon Jan 04 22:43:07 2010 +0100
     1.2 +++ b/src/Pure/context.ML	Mon Jan 04 23:20:35 2010 +0100
     1.3 @@ -574,7 +574,7 @@
     1.4  
     1.5  (** theory data **)
     1.6  
     1.7 -signature OLD_THEORY_DATA_ARGS =
     1.8 +signature THEORY_DATA_PP_ARGS =
     1.9  sig
    1.10    type T
    1.11    val empty: T
    1.12 @@ -582,6 +582,14 @@
    1.13    val merge: Pretty.pp -> T * T -> T
    1.14  end;
    1.15  
    1.16 +signature THEORY_DATA_ARGS =
    1.17 +sig
    1.18 +  type T
    1.19 +  val empty: T
    1.20 +  val extend: T -> T
    1.21 +  val merge: T * T -> T
    1.22 +end;
    1.23 +
    1.24  signature THEORY_DATA =
    1.25  sig
    1.26    type T
    1.27 @@ -590,7 +598,7 @@
    1.28    val map: (T -> T) -> theory -> theory
    1.29  end;
    1.30  
    1.31 -functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
    1.32 +functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
    1.33  struct
    1.34  
    1.35  type T = Data.T;
    1.36 @@ -607,28 +615,14 @@
    1.37  
    1.38  end;
    1.39  
    1.40 -signature THEORY_DATA_ARGS =
    1.41 -sig
    1.42 -  type T
    1.43 -  val empty: T
    1.44 -  val extend: T -> T
    1.45 -  val merge: T * T -> T
    1.46 -end;
    1.47 -
    1.48  functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
    1.49 -struct
    1.50 -
    1.51 -structure Result = TheoryDataFun
    1.52 -(
    1.53 -  type T = Data.T;
    1.54 -  val empty = Data.empty;
    1.55 -  val extend = Data.extend;
    1.56 -  fun merge _ = Data.merge;
    1.57 -);
    1.58 -
    1.59 -open Result;
    1.60 -
    1.61 -end;
    1.62 +  Theory_Data_PP
    1.63 +  (
    1.64 +    type T = Data.T;
    1.65 +    val empty = Data.empty;
    1.66 +    val extend = Data.extend;
    1.67 +    fun merge _ = Data.merge;
    1.68 +  );
    1.69  
    1.70  
    1.71