1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -579,8 +579,8 @@
     1.4  val rel_conversepN = "rel_conversep";
     1.5  val rel_monoN = "rel_mono"
     1.6  val rel_mono_strongN = "rel_mono_strong"
     1.7 -val rel_OON = "rel_compp";
     1.8 -val rel_OO_GrpN = "rel_compp_Grp";
     1.9 +val rel_comppN = "rel_compp";
    1.10 +val rel_compp_GrpN = "rel_compp_Grp";
    1.11  
    1.12  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
    1.13  
    1.14 @@ -638,14 +638,14 @@
    1.15              (map_cong0N, [#map_cong0 axioms], []),
    1.16              (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
    1.17              (map_idN, [Lazy.force (#map_id facts)], []),
    1.18 +            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
    1.19 +            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
    1.20 +            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
    1.21              (rel_eqN, [Lazy.force (#rel_eq facts)], []),
    1.22              (rel_flipN, [Lazy.force (#rel_flip facts)], []),
    1.23 -            (set_mapN, map Lazy.force (#set_map facts), []),
    1.24 -            (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []),
    1.25              (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
    1.26 -            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
    1.27              (rel_monoN, [Lazy.force (#rel_mono facts)], []),
    1.28 -            (rel_OON, [Lazy.force (#rel_OO facts)], [])]
    1.29 +            (set_mapN, map Lazy.force (#set_map facts), [])]
    1.30              |> filter_out (null o #2)
    1.31              |> map (fn (thmN, thms, attrs) =>
    1.32                ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),