unfold intermediate definitions (stemming from composition) in lifted bnf operations

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