# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID a00110bdb4a3ffe0ac78dffdf0343957ebc4a091
# Parent  ef0074e812cd606a9f2574fc765fd5263622bf70
keep all 'ctr' theorems

diff -r ef0074e812cd -r a00110bdb4a3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -1371,12 +1371,11 @@
 
         val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
           (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
-        val ctr_thmss' = map (map snd) ctr_alists;
-        val ctr_thmss = map (map snd o order_list) ctr_alists;
+        val ctr_thmss0 = map (map snd) ctr_alists;
+        val ctr_thmss = map (map (snd o snd) o sort (int_ord o pairself fst)) ctr_alists;
 
         val code_thmss =
-          @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
-            ctr_specss;
+          @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss0 ctr_specss;
 
         val disc_iff_or_disc_thmss =
           map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;