--- a/src/HOL/Tools/Datatype/datatype_selectors.ML	Mon Sep 27 16:32:48 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_selectors.ML	Tue Sep 28 08:35:00 2010 +0200
@@ -26,7 +26,7 @@
   type T = string Stringinttab.table
   val empty = Stringinttab.empty
   val extend = I
-  val merge = Stringinttab.merge (K true)
+  fun merge data : T = Stringinttab.merge (K true) data
 )
 
 fun pretty_term context = Syntax.pretty_term (Context.proof_of context)