author | blanchet |
Tue, 21 Jan 2014 14:52:23 +0100 | |
changeset 55099 | 79c92e2dc359 |
parent 55098 | 01869d711567 |
child 55100 | 697b41533e1a |
--- 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)) =