added collection theorem for consistency and convenience

--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:19:58 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:20:13 2014 +0200
@@ -831,6 +831,8 @@
 \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
 @{thm list.split_sel_asm[no_vars]}
 
+\item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]
+
 \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
 @{thm list.case_eq_if[no_vars]}
 

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:13 2014 +0200
@@ -216,6 +216,7 @@
 val split_selN = "split_sel";
 val split_sel_asmN = "split_sel_asm";
 val splitsN = "splits";
+val split_selsN = "split_sels";
 val case_cong_weak_thmsN = "case_cong_weak";
 
 val cong_attrs = @{attributes [cong]};
@@ -987,7 +988,8 @@
            (split_sel_asmN, split_sel_asm_thms, []),
            (splitN, [split_thm], []),
            (split_asmN, [split_asm_thm], []),
-           (splitsN, [split_thm, split_asm_thm], [])]
+           (splitsN, [split_thm, split_asm_thm], []),
+           (split_selsN, split_sel_thms @ split_sel_asm_thms, [])]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
             ((qualify true (Binding.name thmN), attrs), [(thms, [])]));