# 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