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