# HG changeset patch
# User blanchet
# Date 1285655700 -7200
# Node ID a727e1dab1627a3621e596a3dc0020142ff17227
# Parent  b4e131840b2abc2583d99de1d5a4549273d30aa5
make SML/NJ happy

diff -r b4e131840b2a -r a727e1dab162 src/HOL/Tools/Datatype/datatype_selectors.ML
--- 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)