# 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;