# HG changeset patch
# User wenzelm
# Date 1254263239 -7200
# Node ID c6e6a4665ff5f46e5f89b9bbc3b06e8a77b29b30
# Parent  511e6976f0318f2ebf95ba231f66d7cb9179a318
made SML/NJ happy;

diff -r 511e6976f031 -r c6e6a4665ff5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Sep 30 00:17:06 2009 +0200
+++ b/src/HOL/Tools/record.ML	Wed Sep 30 00:27:19 2009 +0200
@@ -104,7 +104,7 @@
   val empty = Symtab.make [tuple_istuple];
   val copy = I;
   val extend = I;
-  val merge = K (Symtab.merge Thm.eq_thm_prop);
+  fun merge _ = Symtab.merge Thm.eq_thm_prop;
 );
 
 fun do_typedef name repT alphas thy =