# HG changeset patch
# User blanchet
# Date 1390295211 -3600
# Node ID a4eafd0db804a7c1b64a518f24c927b04e60cd8b
# Parent  f05b42b908f426be0f1a648bc1fdcd0a86ca1ee5
made SML/NJ happier

diff -r f05b42b908f4 -r a4eafd0db804 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 07:18:05 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 10:06:51 2014 +0100
@@ -365,7 +365,7 @@
    (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss,
     disc_iter_iff_attrs),
    (map (map (map (Morphism.thm phi))) sel_unfoldsss,
-    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
+    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
 
 val transfer_gfp_sugar_thms =
   morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;