made smlnj happy
authorhaftmann
Fri, 19 Nov 2010 10:37:06 +0100
changeset 40614 d6eeffa0d9a0
parent 40613 23626b388e07
child 40615 ab551d108feb
made smlnj happy
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
 );