made SML/NJ happier
authorblanchet
Tue, 21 Jan 2014 14:52:23 +0100
changeset 5644179c92e2dc359
parent 56440 01869d711567
child 56442 697b41533e1a
made SML/NJ happier
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jan 21 13:51:10 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Jan 21 14:52:23 2014 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4    type T = n2m_sugar Typtab.table;
     1.5    val empty = Typtab.empty;
     1.6    val extend = I;
     1.7 -  val merge = Typtab.merge (eq_fst (eq_list eq_fp_sugar));
     1.8 +  fun merge data : T = Typtab.merge (eq_fst (eq_list eq_fp_sugar)) data;
     1.9  );
    1.10  
    1.11  fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =