src/Tools/value.ML
changeset 29288 253bcf2a5854
parent 28952 15a4b2cf8c34
child 31218 fa54c1e614df
     1.1 --- a/src/Tools/value.ML	Thu Jan 01 14:23:39 2009 +0100
     1.2 +++ b/src/Tools/value.ML	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    val empty = [];
     1.5    val copy = I;
     1.6    val extend = I;
     1.7 -  fun merge pp = AList.merge (op =) (K true);
     1.8 +  fun merge _ data = AList.merge (op =) (K true) data;
     1.9  )
    1.10  
    1.11  val add_evaluator = Evaluator.map o AList.update (op =);