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
 );