# HG changeset patch
# User traytel
# Date 1439477220 -7200
# Node ID 141a1d4852595a1fe425f52f8c7f85bd0de4919a
# Parent  6584c0f3f0e06424de0039dd0c389e86d691e2eb
unfold intermediate definitions (stemming from composition) in lifted bnf operations

diff -r 6584c0f3f0e0 -r 141a1d485259 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Thu Aug 13 13:55:52 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Thu Aug 13 16:47:00 2015 +0200
@@ -299,6 +299,8 @@
             tactics wit_tac NONE map_b rel_b set_bs
             ((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G)
             lthy;
+
+          val bnf = morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf;
         in
           lthy |> BNF_Def.register_bnf plugins AbsT_name bnf
         end
@@ -388,4 +390,4 @@
     ((parse_plugins -- parse_type_args_named_constrained -- Parse.type_const --
       parse_typedef_thm -- parse_map_rel_bindings) >> copy_bnf_cmd);
 
-end
\ No newline at end of file
+end