src/HOL/Tools/BNF/bnf_lift.ML
changeset 66272 c6714a9562ae
parent 63023 1f4b011c5738
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jul 11 20:47:19 2017 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jul 11 21:36:42 2017 +0200
     1.3 @@ -326,12 +326,14 @@
     1.4                [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @
     1.5                [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
     1.6  
     1.7 -            val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) false I
     1.8 +            val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
     1.9                tactics wit_tac NONE map_b rel_b pred_b set_bs
    1.10                (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
    1.11                lthy;
    1.12  
    1.13 -            val bnf = morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf;
    1.14 +            val (bnf, lthy) =
    1.15 +              morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf
    1.16 +              |> (fn bnf => note_bnf_defs bnf lthy);
    1.17            in
    1.18              lthy |> BNF_Def.register_bnf plugins AbsT_name bnf
    1.19            end