src/Pure/context.ML
changeset 34253 5930c6391126
parent 34245 25bd3ed2ac9f
child 34259 2ba492b8b6e8
     1.1 --- a/src/Pure/context.ML	Mon Jan 04 19:44:46 2010 +0100
     1.2 +++ b/src/Pure/context.ML	Mon Jan 04 20:25:56 2010 +0100
     1.3 @@ -426,9 +426,9 @@
     1.4  val declare = declare_theory_data;
     1.5  
     1.6  fun get k dest thy =
     1.7 -  dest (case Datatab.lookup (data_of thy) k of
     1.8 +  (case Datatab.lookup (data_of thy) k of
     1.9      SOME x => x
    1.10 -  | NONE => invoke_empty k);   (*adhoc value*)
    1.11 +  | NONE => invoke_empty k) |> dest;
    1.12  
    1.13  fun put k mk x = modify_thy (Datatab.update (k, mk x));
    1.14  
    1.15 @@ -582,16 +582,15 @@
    1.16    val merge: Pretty.pp -> T * T -> T
    1.17  end;
    1.18  
    1.19 -signature OLD_THEORY_DATA =
    1.20 +signature THEORY_DATA =
    1.21  sig
    1.22    type T
    1.23    val get: theory -> T
    1.24    val put: T -> theory -> theory
    1.25    val map: (T -> T) -> theory -> theory
    1.26 -  val init: theory -> theory
    1.27  end;
    1.28  
    1.29 -functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): OLD_THEORY_DATA =
    1.30 +functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
    1.31  struct
    1.32  
    1.33  type T = Data.T;
    1.34 @@ -606,8 +605,6 @@
    1.35  val put = Context.Theory_Data.put kind Data;
    1.36  fun map f thy = put (f (get thy)) thy;
    1.37  
    1.38 -fun init thy = map I thy;
    1.39 -
    1.40  end;
    1.41  
    1.42  signature THEORY_DATA_ARGS =
    1.43 @@ -618,14 +615,6 @@
    1.44    val merge: T * T -> T
    1.45  end;
    1.46  
    1.47 -signature THEORY_DATA =
    1.48 -sig
    1.49 -  type T
    1.50 -  val get: theory -> T
    1.51 -  val put: T -> theory -> theory
    1.52 -  val map: (T -> T) -> theory -> theory
    1.53 -end;
    1.54 -
    1.55  functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
    1.56  struct
    1.57