src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57985 1e93e5265dc2
parent 57984 cbe9a16f8e11
child 58115 bfde04fc5190
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:20:14 2014 +0200
     1.3 @@ -984,12 +984,12 @@
     1.4             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
     1.5             (nchotomyN, [nchotomy_thm], []),
     1.6             (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
     1.7 +           (splitN, [split_thm], []),
     1.8 +           (split_asmN, [split_asm_thm], []),
     1.9             (split_selN, split_sel_thms, []),
    1.10             (split_sel_asmN, split_sel_asm_thms, []),
    1.11 -           (splitN, [split_thm], []),
    1.12 -           (split_asmN, [split_asm_thm], []),
    1.13 -           (splitsN, [split_thm, split_asm_thm], []),
    1.14 -           (split_selsN, split_sel_thms @ split_sel_asm_thms, [])]
    1.15 +           (split_selsN, split_sel_thms @ split_sel_asm_thms, []),
    1.16 +           (splitsN, [split_thm, split_asm_thm], [])]
    1.17            |> filter_out (null o #2)
    1.18            |> map (fn (thmN, thms, attrs) =>
    1.19              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));