# HG changeset patch
# User berghofe
# Date 1116183850 -7200
# Node ID 24c6b96b4a2f6b2f64f4ba54db7f0f33153cb2b4
# Parent  9bd6550dc004da99a05c5837f34681383b697747
Eta-expanded merge function (to make SmlNJ happy).

diff -r 9bd6550dc004 -r 24c6b96b4a2f src/Pure/Isar/term_style.ML
--- a/src/Pure/Isar/term_style.ML	Sat May 14 21:31:13 2005 +0200
+++ b/src/Pure/Isar/term_style.ML	Sun May 15 21:04:10 2005 +0200
@@ -22,7 +22,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge (K true);
+  fun merge x = Symtab.merge (K true) x;
   fun print _ table =
     Pretty.strs ("defined styles:" :: (Symtab.keys table))
     |> Pretty.writeln;