# HG changeset patch
# User haftmann
# Date 1290159426 -3600
# Node ID d6eeffa0d9a0c4d652fd0d24880e074b6870fa4f
# Parent  23626b388e0715356a24cfb68ea2dc6c4b416358
made smlnj happy

diff -r 23626b388e07 -r d6eeffa0d9a0 src/HOL/Tools/functorial_mappers.ML
--- a/src/HOL/Tools/functorial_mappers.ML	Fri Nov 19 10:04:08 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML	Fri Nov 19 10:37:06 2010 +0100
@@ -30,7 +30,7 @@
 structure Data = Theory_Data(
   type T = entry Symtab.table
   val empty = Symtab.empty
-  val merge = Symtab.merge (K true)
+  fun merge (xy : T * T) = Symtab.merge (K true) xy
   val extend = I
 );