src/HOL/Tools/semiring_normalizer.ML
changeset 36771 3e08b6789e66
parent 36754 5ce217fc769a
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Sat May 08 21:25:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 08 22:29:44 2010 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    type T = (thm * entry) list;
     1.5    val empty = [];
     1.6    val extend = I;
     1.7 -  val merge = AList.merge Thm.eq_thm (K true);
     1.8 +  fun merge data = AList.merge Thm.eq_thm (K true) data;
     1.9  );
    1.10  
    1.11  val get = Data.get o Context.Proof;