1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 14:11:26 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 14:33:20 2013 +0100
     1.3 @@ -350,7 +350,7 @@
     1.4  custom names. In the example below, the familiar names @{text null}, @{text hd},
     1.5  @{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
     1.6  default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
     1.7 -@{text list_set}, @{text list_map}, and @{text list_rel}:
     1.8 +@{text set_list}, @{text map_list}, and @{text rel_list}:
     1.9  *}
    1.10  
    1.11  (*<*)
    1.12 @@ -501,7 +501,7 @@
    1.13  reference manual \cite{isabelle-isar-ref}.
    1.14  
    1.15  The optional names preceding the type variables allow to override the default
    1.16 -names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
    1.17 +names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
    1.18  Inside a mutually recursive specification, all defined datatypes must
    1.19  mention exactly the same type variables in the same order.
    1.20  
    1.21 @@ -626,7 +626,7 @@
    1.22  \begin{itemize}
    1.23  \setlength{\itemsep}{0pt}
    1.24  
    1.25 -\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
    1.26 +\item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar
    1.27  @{text case}--@{text of} syntax)
    1.28  
    1.29  \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
    1.30 @@ -638,22 +638,22 @@
    1.31  \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
    1.32  
    1.33  \item \relax{Set functions} (or \relax{natural transformations}):
    1.34 -@{text t_set1}, \ldots, @{text t_setm}
    1.35 -
    1.36 -\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
    1.37 -
    1.38 -\item \relax{Relator}: @{text t_rel}
    1.39 -
    1.40 -\item \relax{Iterator}: @{text t_fold}
    1.41 -
    1.42 -\item \relax{Recursor}: @{text t_rec}
    1.43 +@{text set1_t}, \ldots, @{text t.setm_t}
    1.44 +
    1.45 +\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
    1.46 +
    1.47 +\item \relax{Relator}: @{text t.rel_t}
    1.48 +
    1.49 +\item \relax{Iterator}: @{text t.t_fold}
    1.50 +
    1.51 +\item \relax{Recursor}: @{text t.t_rec}
    1.52  
    1.53  \end{itemize}
    1.54  
    1.55  \noindent
    1.56  The case combinator, discriminators, and selectors are collectively called
    1.57  \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
    1.58 -name and is normally hidden.
    1.59 +names and is normally hidden.
    1.60  *}
    1.61  
    1.62  
    1.63 @@ -810,8 +810,8 @@
    1.64  \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
    1.65  @{thm list.sel_split_asm[no_vars]}
    1.66  
    1.67 -\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\
    1.68 -@{thm list.case_if[no_vars]}
    1.69 +\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
    1.70 +@{thm list.case_eq_if[no_vars]}
    1.71  
    1.72  \end{description}
    1.73  \end{indentblock}
    1.74 @@ -1150,13 +1150,13 @@
    1.75  \noindent
    1.76  The next example features recursion through the @{text option} type. Although
    1.77  @{text option} is not a new-style datatype, it is registered as a BNF with the
    1.78 -map function @{const option_map}:
    1.79 +map function @{const map_option}:
    1.80  *}
    1.81  
    1.82      primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
    1.83        "sum_btree (BNode a lt rt) =
    1.84 -         a + the_default 0 (option_map sum_btree lt) +
    1.85 -           the_default 0 (option_map sum_btree rt)"
    1.86 +         a + the_default 0 (map_option sum_btree lt) +
    1.87 +           the_default 0 (map_option sum_btree rt)"
    1.88  
    1.89  text {*
    1.90  \noindent

     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Tue Nov 19 14:11:26 2013 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Tue Nov 19 14:33:20 2013 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4     expands = [],
     2.5     sel_splits = [],
     2.6     sel_split_asms = [],
     2.7 -   case_ifs = []};
     2.8 +   case_eq_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	Tue Nov 19 14:11:26 2013 +0100
     3.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 14:33:20 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_ifs: thm list};
     3.8 +     case_eq_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_ifs: thm list};
    3.17 +   case_eq_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_ifs} =
    3.26 +    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_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_ifs = map (Morphism.thm phi) case_ifs};
    3.35 +   case_eq_ifs = map (Morphism.thm phi) case_eq_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_ifN = "case_if";
    3.44 +val case_eq_ifN = "case_eq_if";
    3.45  val collapseN = "collapse";
    3.46  val disc_excludeN = "disc_exclude";
    3.47  val disc_exhaustN = "disc_exhaust";
    3.48 @@ -657,7 +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, case_if_thms) =
    3.53 +             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    3.54            if no_discs_sels then
    3.55              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    3.56            else
    3.57 @@ -861,12 +861,12 @@
    3.58                    (thm, asm_thm)
    3.59                  end;
    3.60  
    3.61 -              val case_if_thm =
    3.62 +              val case_eq_if_thm =
    3.63                  let
    3.64                    val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
    3.65                  in
    3.66                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    3.67 -                    mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    3.68 +                    mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
    3.69                    |> Thm.close_derivation
    3.70                    |> singleton (Proof_Context.export names_lthy lthy)
    3.71                  end;
    3.72 @@ -874,7 +874,7 @@
    3.73                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    3.74                 nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
    3.75                 all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
    3.76 -               [sel_split_asm_thm], [case_if_thm])
    3.77 +               [sel_split_asm_thm], [case_eq_if_thm])
    3.78              end;
    3.79  
    3.80          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    3.81 @@ -890,7 +890,7 @@
    3.82          val notes =
    3.83            [(caseN, case_thms, code_nitpicksimp_simp_attrs),
    3.84             (case_congN, [case_cong_thm], []),
    3.85 -           (case_ifN, case_if_thms, []),
    3.86 +           (case_eq_ifN, case_eq_if_thms, []),
    3.87             (collapseN, safe_collapse_thms, simp_attrs),
    3.88             (discN, nontriv_disc_thms, simp_attrs),
    3.89             (discIN, nontriv_discI_thms, []),
    3.90 @@ -921,7 +921,7 @@
    3.91             discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    3.92             sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    3.93             sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    3.94 -           case_ifs = case_if_thms};
    3.95 +           case_eq_ifs = case_eq_if_thms};
    3.96        in
    3.97          (ctr_sugar,
    3.98           lthy

     4.1 --- a/src/HOL/Tools/ctr_sugar_tactics.ML	Tue Nov 19 14:11:26 2013 +0100
     4.2 +++ b/src/HOL/Tools/ctr_sugar_tactics.ML	Tue Nov 19 14:33:20 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_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
     4.8 -    tactic
     4.9 +  val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
    4.10 +    thm list list -> 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 @@ -28,8 +28,8 @@
    4.15    val mk_nchotomy_tac: int -> thm -> tactic
    4.16    val mk_other_half_disc_exclude_tac: thm -> tactic
    4.17    val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
    4.18 -  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
    4.19 -    list list -> tactic
    4.20 +  val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
    4.21 +    thm list list list -> tactic
    4.22    val mk_split_asm_tac: Proof.context -> thm -> tactic
    4.23    val mk_unique_disc_def_tac: int -> thm -> tactic
    4.24  end;
    4.25 @@ -143,17 +143,17 @@
    4.26           else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
    4.27    end;
    4.28  
    4.29 -fun mk_case_if_tac ctxt n uexhaust cases discss' selss =
    4.30 +fun mk_case_cong_tac ctxt uexhaust cases =
    4.31 +  HEADGOAL (rtac uexhaust THEN'
    4.32 +    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
    4.33 +
    4.34 +fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss =
    4.35    HEADGOAL (rtac uexhaust THEN'
    4.36      EVERY' (map3 (fn casex => fn if_discs => fn sels =>
    4.37          EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
    4.38            rtac casex])
    4.39        cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
    4.40  
    4.41 -fun mk_case_cong_tac ctxt uexhaust cases =
    4.42 -  HEADGOAL (rtac uexhaust THEN'
    4.43 -    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
    4.44 -
    4.45  fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
    4.46    HEADGOAL (rtac uexhaust) THEN
    4.47    ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
    4.48 @@ -169,4 +169,4 @@
    4.49  
    4.50  end;
    4.51  
    4.52 -structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;
    4.53 +structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;

     5.1 --- a/src/HOL/Tools/ctr_sugar_util.ML	Tue Nov 19 14:11:26 2013 +0100
     5.2 +++ b/src/HOL/Tools/ctr_sugar_util.ML	Tue Nov 19 14:33:20 2013 +0100
     5.3 @@ -176,9 +176,7 @@
     5.4  fun rapp u t = betapply (t, u);
     5.5  
     5.6  fun list_quant_free quant_const =
     5.7 -  fold_rev (fn free => fn P =>
     5.8 -    let val (x, T) = Term.dest_Free free;
     5.9 -    in quant_const T $ Term.absfree (x, T) P end);
    5.10 +  fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P);
    5.11  
    5.12  val list_all_free = list_quant_free HOLogic.all_const;
    5.13  val list_exists_free = list_quant_free HOLogic.exists_const;