--- 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, [])]));