src/HOL/Codatatype/Tools/bnf_comp.ML
changeset 49018 b2884253b421
parent 49016 640ce226a973
child 49019 fc4decdba5ce
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.8 +      bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.9          ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy;
    1.10  
    1.11      val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
    1.12 @@ -368,7 +368,7 @@
    1.13      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.14  
    1.15      val (bnf', lthy') =
    1.16 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.17 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.18          ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy;
    1.19  
    1.20      val rel_Gr = rel_Gr_of_bnf bnf RS sym;
    1.21 @@ -473,7 +473,7 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.26 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.27          ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy;
    1.28  
    1.29      val liftN_rel_unfold_thm =
    1.30 @@ -561,7 +561,7 @@
    1.31      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.32  
    1.33      val (bnf', lthy') =
    1.34 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.35 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.36          ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy;
    1.37  
    1.38      val permute_rel_unfold_thm =
    1.39 @@ -716,7 +716,7 @@
    1.40  
    1.41      fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
    1.42  
    1.43 -    val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
    1.44 +    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
    1.45          ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
    1.46  
    1.47      val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');