# HG changeset patch
# User wenzelm
# Date 1273350584 -7200
# Node ID 3e08b6789e66b3bcf85ba424079271778c2e708e
# Parent  40837a7b32a7c7aa5dc6793e6de3f9b6b56b5fb9
made SML/NJ happy;

diff -r 40837a7b32a7 -r 3e08b6789e66 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Sat May 08 21:25:25 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sat May 08 22:29:44 2010 +0200
@@ -57,7 +57,7 @@
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
-  val merge = AList.merge Thm.eq_thm (K true);
+  fun merge data = AList.merge Thm.eq_thm (K true) data;
 );
 
 val get = Data.get o Context.Proof;