# HG changeset patch
# User traytel
# Date 1390307270 -3600
# Node ID 81dac5c1a5bb4f97ab4814b0ee8131bb6d40a3cf
# Parent  916b2ac758f4418750ffa20aa0d5626de6b2886d# Parent  7883bd17362fad0d6ba86569dbb9dd783b66b0f5
merged

diff -r 916b2ac758f4 -r 81dac5c1a5bb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:21:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:27:50 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;