1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 13 10:53:36 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 13 12:32:26 2013 +0100
     1.3 @@ -810,8 +810,8 @@
     1.4  \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
     1.5  @{thm list.sel_split_asm[no_vars]}
     1.6  
     1.7 -\item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
     1.8 -@{thm list.case_conv_if[no_vars]}
     1.9 +\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\
    1.10 +@{thm list.case_if[no_vars]}
    1.11  
    1.12  \end{description}
    1.13  \end{indentblock}

     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 13 10:53:36 2013 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 13 12:32:26 2013 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4     expands = [],
     2.5     sel_splits = [],
     2.6     sel_split_asms = [],
     2.7 -   case_conv_ifs = []};
     2.8 +   case_ifs = []};
     2.9  
    2.10  fun register dt_infos =
    2.11    Data.map (fn {types, constrs, cases} =>

     3.1 --- a/src/HOL/Tools/ctr_sugar.ML	Wed Nov 13 10:53:36 2013 +0100
     3.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Wed Nov 13 12:32:26 2013 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4       expands: thm list,
     3.5       sel_splits: thm list,
     3.6       sel_split_asms: thm list,
     3.7 -     case_conv_ifs: thm list};
     3.8 +     case_ifs: thm list};
     3.9  
    3.10    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
    3.11    val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
    3.12 @@ -90,7 +90,7 @@
    3.13     expands: thm list,
    3.14     sel_splits: thm list,
    3.15     sel_split_asms: thm list,
    3.16 -   case_conv_ifs: thm list};
    3.17 +   case_ifs: thm list};
    3.18  
    3.19  fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
    3.20      {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
    3.21 @@ -98,7 +98,7 @@
    3.22  
    3.23  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    3.24      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    3.25 -    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_conv_ifs} =
    3.26 +    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} =
    3.27    {ctrs = map (Morphism.term phi) ctrs,
    3.28     casex = Morphism.term phi casex,
    3.29     discs = map (Morphism.term phi) discs,
    3.30 @@ -121,7 +121,7 @@
    3.31     expands = map (Morphism.thm phi) expands,
    3.32     sel_splits = map (Morphism.thm phi) sel_splits,
    3.33     sel_split_asms = map (Morphism.thm phi) sel_split_asms,
    3.34 -   case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
    3.35 +   case_ifs = map (Morphism.thm phi) case_ifs};
    3.36  
    3.37  val transfer_ctr_sugar =
    3.38    morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    3.39 @@ -160,7 +160,7 @@
    3.40  
    3.41  val caseN = "case";
    3.42  val case_congN = "case_cong";
    3.43 -val case_conv_ifN = "case_conv_if";
    3.44 +val case_ifN = "case_if";
    3.45  val collapseN = "collapse";
    3.46  val disc_excludeN = "disc_exclude";
    3.47  val disc_exhaustN = "disc_exhaust";
    3.48 @@ -657,8 +657,7 @@
    3.49  
    3.50          val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
    3.51               disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
    3.52 -             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
    3.53 -             case_conv_if_thms) =
    3.54 +             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) =
    3.55            if no_discs_sels then
    3.56              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    3.57            else
    3.58 @@ -862,12 +861,12 @@
    3.59                    (thm, asm_thm)
    3.60                  end;
    3.61  
    3.62 -              val case_conv_if_thm =
    3.63 +              val case_if_thm =
    3.64                  let
    3.65                    val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
    3.66                  in
    3.67                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    3.68 -                    mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    3.69 +                    mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    3.70                    |> Thm.close_derivation
    3.71                    |> singleton (Proof_Context.export names_lthy lthy)
    3.72                  end;
    3.73 @@ -875,7 +874,7 @@
    3.74                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    3.75                 nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
    3.76                 all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
    3.77 -               [sel_split_asm_thm], [case_conv_if_thm])
    3.78 +               [sel_split_asm_thm], [case_if_thm])
    3.79              end;
    3.80  
    3.81          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    3.82 @@ -891,7 +890,7 @@
    3.83          val notes =
    3.84            [(caseN, case_thms, code_nitpicksimp_simp_attrs),
    3.85             (case_congN, [case_cong_thm], []),
    3.86 -           (case_conv_ifN, case_conv_if_thms, []),
    3.87 +           (case_ifN, case_if_thms, []),
    3.88             (collapseN, safe_collapse_thms, simp_attrs),
    3.89             (discN, nontriv_disc_thms, simp_attrs),
    3.90             (discIN, nontriv_discI_thms, []),
    3.91 @@ -922,7 +921,7 @@
    3.92             discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    3.93             sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    3.94             sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    3.95 -           case_conv_ifs = case_conv_if_thms};
    3.96 +           case_ifs = case_if_thms};
    3.97        in
    3.98          (ctr_sugar,
    3.99           lthy

     4.1 --- a/src/HOL/Tools/ctr_sugar_tactics.ML	Wed Nov 13 10:53:36 2013 +0100
     4.2 +++ b/src/HOL/Tools/ctr_sugar_tactics.ML	Wed Nov 13 12:32:26 2013 +0100
     4.3 @@ -18,8 +18,8 @@
     4.4    val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
     4.5    val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
     4.6    val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
     4.7 -  val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
     4.8 -    thm list list -> tactic
     4.9 +  val mk_case_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
    4.10 +    tactic
    4.11    val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    4.12    val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    4.13    val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    4.14 @@ -143,7 +143,7 @@
    4.15           else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
    4.16    end;
    4.17  
    4.18 -fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
    4.19 +fun mk_case_if_tac ctxt n uexhaust cases discss' selss =
    4.20    HEADGOAL (rtac uexhaust THEN'
    4.21      EVERY' (map3 (fn casex => fn if_discs => fn sels =>
    4.22          EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),