src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57984 cbe9a16f8e11
parent 57983 6edc3529bb4e
child 57985 1e93e5265dc2
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:13 2014 +0200
     1.3 @@ -216,6 +216,7 @@
     1.4  val split_selN = "split_sel";
     1.5  val split_sel_asmN = "split_sel_asm";
     1.6  val splitsN = "splits";
     1.7 +val split_selsN = "split_sels";
     1.8  val case_cong_weak_thmsN = "case_cong_weak";
     1.9  
    1.10  val cong_attrs = @{attributes [cong]};
    1.11 @@ -987,7 +988,8 @@
    1.12             (split_sel_asmN, split_sel_asm_thms, []),
    1.13             (splitN, [split_thm], []),
    1.14             (split_asmN, [split_asm_thm], []),
    1.15 -           (splitsN, [split_thm, split_asm_thm], [])]
    1.16 +           (splitsN, [split_thm, split_asm_thm], []),
    1.17 +           (split_selsN, split_sel_thms @ split_sel_asm_thms, [])]
    1.18            |> filter_out (null o #2)
    1.19            |> map (fn (thmN, thms, attrs) =>
    1.20              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));