src/Tools/value.ML
changeset 33522 737589bb9bb8
parent 31218 fa54c1e614df
child 36960 01594f816e3a
     1.1 --- a/src/Tools/value.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Tools/value.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -15,12 +15,12 @@
     1.4  structure Value : VALUE =
     1.5  struct
     1.6  
     1.7 -structure Evaluator = TheoryDataFun(
     1.8 +structure Evaluator = Theory_Data
     1.9 +(
    1.10    type T = (string * (Proof.context -> term -> term)) list;
    1.11    val empty = [];
    1.12 -  val copy = I;
    1.13    val extend = I;
    1.14 -  fun merge _ data = AList.merge (op =) (K true) data;
    1.15 +  fun merge data : T = AList.merge (op =) (K true) data;
    1.16  )
    1.17  
    1.18  val add_evaluator = Evaluator.map o AList.update (op =);