# HG changeset patch
# User blanchet
# Date 1390312343 -3600
# Node ID 79c92e2dc35934b5a6ed1bba3bf58ea18ce54895
# Parent  01869d7115678695339264ddd77f7d7c2b28bb04
made SML/NJ happier

diff -r 01869d711567 -r 79c92e2dc359 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jan 21 13:51:10 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jan 21 14:52:23 2014 +0100
@@ -43,7 +43,7 @@
   type T = n2m_sugar Typtab.table;
   val empty = Typtab.empty;
   val extend = I;
-  val merge = Typtab.merge (eq_fst (eq_list eq_fp_sugar));
+  fun merge data : T = Typtab.merge (eq_fst (eq_list eq_fp_sugar)) data;
 );
 
 fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =