# HG changeset patch
# User blanchet
# Date 1408375214 -7200
# Node ID 1e93e5265dc285e7bc0e56dc406112bc0c94157c
# Parent  cbe9a16f8e1139cc72bab178531d6f459b6cd017
tuning

diff -r cbe9a16f8e11 -r 1e93e5265dc2 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:13 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:14 2014 +0200
@@ -984,12 +984,12 @@
            (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
            (nchotomyN, [nchotomy_thm], []),
            (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
+           (splitN, [split_thm], []),
+           (split_asmN, [split_asm_thm], []),
            (split_selN, split_sel_thms, []),
            (split_sel_asmN, split_sel_asm_thms, []),
-           (splitN, [split_thm], []),
-           (split_asmN, [split_asm_thm], []),
-           (splitsN, [split_thm, split_asm_thm], []),
-           (split_selsN, split_sel_thms @ split_sel_asm_thms, [])]
+           (split_selsN, split_sel_thms @ split_sel_asm_thms, []),
+           (splitsN, [split_thm, split_asm_thm], [])]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));