1.1 --- a/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 13:38:55 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Fri Oct 18 14:58:02 2013 +0200
     1.3 @@ -177,7 +177,8 @@
     1.4  val inductsimp_attrs = @{attributes [induct_simp]};
     1.5  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
     1.6  val simp_attrs = @{attributes [simp]};
     1.7 -val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
     1.8 +val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
     1.9 +val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
    1.10  
    1.11  fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
    1.12  
    1.13 @@ -869,6 +870,13 @@
    1.14          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.15          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
    1.16  
    1.17 +        val anonymous_notes =
    1.18 +          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
    1.19 +           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
    1.20 +              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
    1.21 +            code_nitpicksimp_attrs)]
    1.22 +          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.23 +
    1.24          val notes =
    1.25            [(caseN, case_thms, code_nitpicksimp_simp_attrs),
    1.26             (case_congN, [case_cong_thm], []),
    1.27 @@ -895,10 +903,6 @@
    1.28            |> map (fn (thmN, thms, attrs) =>
    1.29              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
    1.30  
    1.31 -        val anonymous_notes =
    1.32 -          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
    1.33 -          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    1.34 -
    1.35          val ctr_sugar =
    1.36            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    1.37             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,