1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 14:11:26 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 14:33:20 2013 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4       expands: thm list,
     1.5       sel_splits: thm list,
     1.6       sel_split_asms: thm list,
     1.7 -     case_ifs: thm list};
     1.8 +     case_eq_ifs: thm list};
     1.9  
    1.10    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
    1.11    val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
    1.12 @@ -90,7 +90,7 @@
    1.13     expands: thm list,
    1.14     sel_splits: thm list,
    1.15     sel_split_asms: thm list,
    1.16 -   case_ifs: thm list};
    1.17 +   case_eq_ifs: thm list};
    1.18  
    1.19  fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
    1.20      {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
    1.21 @@ -98,7 +98,7 @@
    1.22  
    1.23  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.24      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    1.25 -    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} =
    1.26 +    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
    1.27    {ctrs = map (Morphism.term phi) ctrs,
    1.28     casex = Morphism.term phi casex,
    1.29     discs = map (Morphism.term phi) discs,
    1.30 @@ -121,7 +121,7 @@
    1.31     expands = map (Morphism.thm phi) expands,
    1.32     sel_splits = map (Morphism.thm phi) sel_splits,
    1.33     sel_split_asms = map (Morphism.thm phi) sel_split_asms,
    1.34 -   case_ifs = map (Morphism.thm phi) case_ifs};
    1.35 +   case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
    1.36  
    1.37  val transfer_ctr_sugar =
    1.38    morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    1.39 @@ -160,7 +160,7 @@
    1.40  
    1.41  val caseN = "case";
    1.42  val case_congN = "case_cong";
    1.43 -val case_ifN = "case_if";
    1.44 +val case_eq_ifN = "case_eq_if";
    1.45  val collapseN = "collapse";
    1.46  val disc_excludeN = "disc_exclude";
    1.47  val disc_exhaustN = "disc_exhaust";
    1.48 @@ -657,7 +657,7 @@
    1.49  
    1.50          val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
    1.51               disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
    1.52 -             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) =
    1.53 +             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    1.54            if no_discs_sels then
    1.55              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    1.56            else
    1.57 @@ -861,12 +861,12 @@
    1.58                    (thm, asm_thm)
    1.59                  end;
    1.60  
    1.61 -              val case_if_thm =
    1.62 +              val case_eq_if_thm =
    1.63                  let
    1.64                    val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
    1.65                  in
    1.66                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.67 -                    mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    1.68 +                    mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    1.69                    |> Thm.close_derivation
    1.70                    |> singleton (Proof_Context.export names_lthy lthy)
    1.71                  end;
    1.72 @@ -874,7 +874,7 @@
    1.73                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    1.74                 nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
    1.75                 all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
    1.76 -               [sel_split_asm_thm], [case_if_thm])
    1.77 +               [sel_split_asm_thm], [case_eq_if_thm])
    1.78              end;
    1.79  
    1.80          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    1.81 @@ -890,7 +890,7 @@
    1.82          val notes =
    1.83            [(caseN, case_thms, code_nitpicksimp_simp_attrs),
    1.84             (case_congN, [case_cong_thm], []),
    1.85 -           (case_ifN, case_if_thms, []),
    1.86 +           (case_eq_ifN, case_eq_if_thms, []),
    1.87             (collapseN, safe_collapse_thms, simp_attrs),
    1.88             (discN, nontriv_disc_thms, simp_attrs),
    1.89             (discIN, nontriv_discI_thms, []),
    1.90 @@ -921,7 +921,7 @@
    1.91             discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    1.92             sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    1.93             sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    1.94 -           case_ifs = case_if_thms};
    1.95 +           case_eq_ifs = case_eq_if_thms};
    1.96        in
    1.97          (ctr_sugar,
    1.98           lthy