shortened generated property name

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

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

--- a/src/HOL/Tools/ctr_sugar.ML	Wed Nov 13 10:53:36 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Wed Nov 13 12:32:26 2013 +0100
@@ -30,7 +30,7 @@
      expands: thm list,
      sel_splits: thm list,
      sel_split_asms: thm list,
-     case_conv_ifs: thm list};
+     case_ifs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
   val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
@@ -90,7 +90,7 @@
    expands: thm list,
    sel_splits: thm list,
    sel_split_asms: thm list,
-   case_conv_ifs: thm list};
+   case_ifs: thm list};
 
 fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
     {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
@@ -98,7 +98,7 @@
 
 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
-    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_conv_ifs} =
+    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} =
   {ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
@@ -121,7 +121,7 @@
    expands = map (Morphism.thm phi) expands,
    sel_splits = map (Morphism.thm phi) sel_splits,
    sel_split_asms = map (Morphism.thm phi) sel_split_asms,
-   case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
+   case_ifs = map (Morphism.thm phi) case_ifs};
 
 val transfer_ctr_sugar =
   morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
@@ -160,7 +160,7 @@
 
 val caseN = "case";
 val case_congN = "case_cong";
-val case_conv_ifN = "case_conv_if";
+val case_ifN = "case_if";
 val collapseN = "collapse";
 val disc_excludeN = "disc_exclude";
 val disc_exhaustN = "disc_exhaust";
@@ -657,8 +657,7 @@
 
         val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
              disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
-             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
-             case_conv_if_thms) =
+             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) =
           if no_discs_sels then
             ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
           else
@@ -862,12 +861,12 @@
                   (thm, asm_thm)
                 end;
 
-              val case_conv_if_thm =
+              val case_if_thm =
                 let
                   val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
                 in
                   Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
-                    mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+                    mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
                   |> Thm.close_derivation
                   |> singleton (Proof_Context.export names_lthy lthy)
                 end;
@@ -875,7 +874,7 @@
               (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
                nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
                all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
-               [sel_split_asm_thm], [case_conv_if_thm])
+               [sel_split_asm_thm], [case_if_thm])
             end;
 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -891,7 +890,7 @@
         val notes =
           [(caseN, case_thms, code_nitpicksimp_simp_attrs),
            (case_congN, [case_cong_thm], []),
-           (case_conv_ifN, case_conv_if_thms, []),
+           (case_ifN, case_if_thms, []),
            (collapseN, safe_collapse_thms, simp_attrs),
            (discN, nontriv_disc_thms, simp_attrs),
            (discIN, nontriv_discI_thms, []),
@@ -922,7 +921,7 @@
            discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
            sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
            sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
-           case_conv_ifs = case_conv_if_thms};
+           case_ifs = case_if_thms};
       in
         (ctr_sugar,
          lthy

--- a/src/HOL/Tools/ctr_sugar_tactics.ML	Wed Nov 13 10:53:36 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_tactics.ML	Wed Nov 13 12:32:26 2013 +0100
@@ -18,8 +18,8 @@
   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
   val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
-    thm list list -> tactic
+  val mk_case_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
+    tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
@@ -143,7 +143,7 @@
          else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
   end;
 
-fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
+fun mk_case_if_tac ctxt n uexhaust cases discss' selss =
   HEADGOAL (rtac uexhaust THEN'
     EVERY' (map3 (fn casex => fn if_discs => fn sels =>
         EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),