# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 56fdc6412abc06470213f3ffdbcc65d0b588e358
# Parent  46494c7dd344b9b35320eb63d18f2f03a816e0ff
tuning

diff -r 46494c7dd344 -r 56fdc6412abc src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -579,8 +579,8 @@
 val rel_conversepN = "rel_conversep";
 val rel_monoN = "rel_mono"
 val rel_mono_strongN = "rel_mono_strong"
-val rel_OON = "rel_compp";
-val rel_OO_GrpN = "rel_compp_Grp";
+val rel_comppN = "rel_compp";
+val rel_compp_GrpN = "rel_compp_Grp";
 
 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 
@@ -638,14 +638,14 @@
             (map_cong0N, [#map_cong0 axioms], []),
             (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
             (map_idN, [Lazy.force (#map_id facts)], []),
+            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
+            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
+            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
             (rel_flipN, [Lazy.force (#rel_flip facts)], []),
-            (set_mapN, map Lazy.force (#set_map facts), []),
-            (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []),
             (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
-            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
             (rel_monoN, [Lazy.force (#rel_mono facts)], []),
-            (rel_OON, [Lazy.force (#rel_OO facts)], [])]
+            (set_mapN, map Lazy.force (#set_map facts), [])]
             |> filter_out (null o #2)
             |> map (fn (thmN, thms, attrs) =>
               ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),