# HG changeset patch
# User blanchet
# Date 1390306382 -3600
# Node ID 7883bd17362fad0d6ba86569dbb9dd783b66b0f5
# Parent  149ccaf4ae5c70a44e59010c338cb93cc6124e44
made SML/NJ happier

diff -r 149ccaf4ae5c -r 7883bd17362f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:13:02 2014 +0100
@@ -341,7 +341,8 @@
 
 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
   ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
-   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
+   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs))
+  : lfp_sugar_thms;
 
 val transfer_lfp_sugar_thms =
   morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;