reordered some (co)datatype property names for more consistency
authorblanchet
Mon Aug 18 17:19:58 2014 +0200 (2014-08-18)
changeset 579836edc3529bb4e
parent 57982 d2bc61d78370
child 57984 cbe9a16f8e11
reordered some (co)datatype property names for more consistency
NEWS
src/Doc/Datatypes/Datatypes.thy
src/Doc/Logics/document/HOL.tex
src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
src/HOL/BNF_Examples/Process.thy
src/HOL/BNF_Examples/Stream.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Conform.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Nat.thy
src/HOL/Old_Number_Theory/Factorization.thy
src/HOL/Product_Type.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/record.ML
     1.1 --- a/NEWS	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/NEWS	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -17,6 +17,28 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New (co)datatype package:
     1.8 +  - Renamed theorems:
     1.9 +      disc_corec ~> corec_disc
    1.10 +      disc_corec_iff ~> corec_disc_iff
    1.11 +      disc_exclude ~> distinct_disc
    1.12 +      disc_exhaust ~> exhaust_disc
    1.13 +      disc_map_iff ~> map_disc_iff
    1.14 +      sel_corec ~> corec_sel
    1.15 +      sel_exhaust ~> exhaust_sel
    1.16 +      sel_map ~> map_sel
    1.17 +      sel_set ~> set_sel
    1.18 +      sel_split ~> split_sel
    1.19 +      sel_split_asm ~> split_sel_asm
    1.20 +      strong_coinduct ~> coinduct_strong
    1.21 +      weak_case_cong ~> case_cong_weak
    1.22 +    INCOMPATIBILITY.
    1.23 +
    1.24 +* Old datatype package:
    1.25 +  - Renamed theorems:
    1.26 +      weak_case_cong ~> case_cong_weak
    1.27 +    INCOMPATIBILITY.
    1.28 +
    1.29  * Sledgehammer:
    1.30    - Minimization is now always enabled by default.
    1.31      Removed subcommand:
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:25 2014 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:19:58 2014 +0200
     2.3 @@ -773,8 +773,8 @@
     2.4  \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
     2.5  @{thm list.case_cong[no_vars]}
     2.6  
     2.7 -\item[@{text "t."}\hthm{weak_case_cong} @{text "[cong]"}\rm:] ~ \\
     2.8 -@{thm list.weak_case_cong[no_vars]}
     2.9 +\item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
    2.10 +@{thm list.case_cong_weak[no_vars]}
    2.11  
    2.12  \item[@{text "t."}\hthm{split}\rm:] ~ \\
    2.13  @{thm list.split[no_vars]}
    2.14 @@ -809,27 +809,27 @@
    2.15  @{thm list.collapse(1)[no_vars]} \\
    2.16  @{thm list.collapse(2)[no_vars]}
    2.17  
    2.18 -\item[@{text "t."}\hthm{disc_exclude} @{text "[dest]"}\rm:] ~ \\
    2.19 +\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
    2.20  These properties are missing for @{typ "'a list"} because there is only one
    2.21  proper discriminator. Had the datatype been introduced with a second
    2.22  discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
    2.23  @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
    2.24  @{prop "nonnull list \<Longrightarrow> \<not> null list"}
    2.25  
    2.26 -\item[@{text "t."}\hthm{disc_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    2.27 -@{thm list.disc_exhaust[no_vars]}
    2.28 -
    2.29 -\item[@{text "t."}\hthm{sel_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    2.30 -@{thm list.sel_exhaust[no_vars]}
    2.31 +\item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    2.32 +@{thm list.exhaust_disc[no_vars]}
    2.33 +
    2.34 +\item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
    2.35 +@{thm list.exhaust_sel[no_vars]}
    2.36  
    2.37  \item[@{text "t."}\hthm{expand}\rm:] ~ \\
    2.38  @{thm list.expand[no_vars]}
    2.39  
    2.40 -\item[@{text "t."}\hthm{sel_split}\rm:] ~ \\
    2.41 -@{thm list.sel_split[no_vars]}
    2.42 -
    2.43 -\item[@{text "t."}\hthm{sel_split_asm}\rm:] ~ \\
    2.44 -@{thm list.sel_split_asm[no_vars]}
    2.45 +\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
    2.46 +@{thm list.split_sel[no_vars]}
    2.47 +
    2.48 +\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
    2.49 +@{thm list.split_sel_asm[no_vars]}
    2.50  
    2.51  \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
    2.52  @{thm list.case_eq_if[no_vars]}
    2.53 @@ -868,18 +868,18 @@
    2.54  @{thm list.set_intros(1)[no_vars]} \\
    2.55  @{thm list.set_intros(2)[no_vars]}
    2.56  
    2.57 -\item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
    2.58 -@{thm list.sel_set[no_vars]}
    2.59 +\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
    2.60 +@{thm list.set_sel[no_vars]}
    2.61  
    2.62  \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
    2.63  @{thm list.map(1)[no_vars]} \\
    2.64  @{thm list.map(2)[no_vars]}
    2.65  
    2.66 -\item[@{text "t."}\hthm{disc_map_iff} @{text "[simp]"}\rm:] ~ \\
    2.67 -@{thm list.disc_map_iff[no_vars]}
    2.68 -
    2.69 -\item[@{text "t."}\hthm{sel_map}\rm:] ~ \\
    2.70 -@{thm list.sel_map[no_vars]}
    2.71 +\item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
    2.72 +@{thm list.map_disc_iff[no_vars]}
    2.73 +
    2.74 +\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
    2.75 +@{thm list.map_sel[no_vars]}
    2.76  
    2.77  \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
    2.78  @{thm list.rel_inject(1)[no_vars]} \\
    2.79 @@ -1772,10 +1772,10 @@
    2.80  @{thm llist.coinduct[no_vars]}
    2.81  
    2.82  \item[\begin{tabular}{@ {}l@ {}}
    2.83 -  @{text "t."}\hthm{strong_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    2.84 -  \phantom{@{text "t."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
    2.85 +  @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    2.86 +  \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
    2.87  \end{tabular}] ~ \\
    2.88 -@{thm llist.strong_coinduct[no_vars]}
    2.89 +@{thm llist.coinduct_strong[no_vars]}
    2.90  
    2.91  \item[\begin{tabular}{@ {}l@ {}}
    2.92    @{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    2.93 @@ -1786,8 +1786,8 @@
    2.94  
    2.95  \item[\begin{tabular}{@ {}l@ {}}
    2.96    @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
    2.97 -  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
    2.98 -  \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{strong_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
    2.99 +  @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
   2.100 +  \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
   2.101    @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
   2.102    \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
   2.103  \end{tabular}] ~ \\
   2.104 @@ -1808,17 +1808,17 @@
   2.105  \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
   2.106  @{thm llist.corec_code[no_vars]}
   2.107  
   2.108 -\item[@{text "t."}\hthm{disc_corec}\rm:] ~ \\
   2.109 -@{thm llist.disc_corec(1)[no_vars]} \\
   2.110 -@{thm llist.disc_corec(2)[no_vars]}
   2.111 -
   2.112 -\item[@{text "t."}\hthm{disc_corec_iff} @{text "[simp]"}\rm:] ~ \\
   2.113 -@{thm llist.disc_corec_iff(1)[no_vars]} \\
   2.114 -@{thm llist.disc_corec_iff(2)[no_vars]}
   2.115 -
   2.116 -\item[@{text "t."}\hthm{sel_corec} @{text "[simp]"}\rm:] ~ \\
   2.117 -@{thm llist.sel_corec(1)[no_vars]} \\
   2.118 -@{thm llist.sel_corec(2)[no_vars]}
   2.119 +\item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
   2.120 +@{thm llist.corec_disc(1)[no_vars]} \\
   2.121 +@{thm llist.corec_disc(2)[no_vars]}
   2.122 +
   2.123 +\item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
   2.124 +@{thm llist.corec_disc_iff(1)[no_vars]} \\
   2.125 +@{thm llist.corec_disc_iff(2)[no_vars]}
   2.126 +
   2.127 +\item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
   2.128 +@{thm llist.corec_sel(1)[no_vars]} \\
   2.129 +@{thm llist.corec_sel(2)[no_vars]}
   2.130  
   2.131  \end{description}
   2.132  \end{indentblock}
   2.133 @@ -1829,7 +1829,7 @@
   2.134  \begin{indentblock}
   2.135  \begin{description}
   2.136  
   2.137 -\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec_iff}] @{text t.sel_corec} ~ \\
   2.138 +\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\
   2.139  @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
   2.140  
   2.141  \end{description}
   2.142 @@ -2151,7 +2151,7 @@
   2.143  @{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
   2.144  @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
   2.145  @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
   2.146 -and analogously for @{text strong_coinduct}. These rules and the
   2.147 +and analogously for @{text coinduct_strong}. These rules and the
   2.148  underlying corecursors are generated on a per-need basis and are kept in a cache
   2.149  to speed up subsequent definitions.
   2.150  *}
     3.1 --- a/src/Doc/Logics/document/HOL.tex	Mon Aug 18 15:03:25 2014 +0200
     3.2 +++ b/src/Doc/Logics/document/HOL.tex	Mon Aug 18 17:19:58 2014 +0200
     3.3 @@ -1709,7 +1709,7 @@
     3.4    the arms of the \texttt{case}-construct exposed and simplified. To ensure
     3.5    full simplification of all parts of a \texttt{case}-construct for datatype
     3.6    $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
     3.7 -  example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
     3.8 +  example by \texttt{delcongs [thm "$t$.case_cong_weak"]}.
     3.9  \end{warn}
    3.10  
    3.11  \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
     4.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Aug 18 15:03:25 2014 +0200
     4.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Aug 18 17:19:58 2014 +0200
     4.3 @@ -75,7 +75,7 @@
     4.4  lemma unfold:
     4.5  "root (unfold rt ct b) = rt b"
     4.6  "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
     4.7 -using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
     4.8 +using dtree.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
     4.9  apply blast
    4.10  unfolding cont_def comp_def
    4.11  by (simp add: case_sum_o_inj map_sum.compositionality image_image)
    4.12 @@ -83,7 +83,7 @@
    4.13  lemma corec:
    4.14  "root (corec rt ct b) = rt b"
    4.15  "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
    4.16 -using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
    4.17 +using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
    4.18  unfolding cont_def comp_def id_def
    4.19  by simp_all
    4.20  
     5.1 --- a/src/HOL/BNF_Examples/Process.thy	Mon Aug 18 15:03:25 2014 +0200
     5.2 +++ b/src/HOL/BNF_Examples/Process.thy	Mon Aug 18 17:19:58 2014 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4  (* Constructors versus discriminators *)
     5.5  theorem isAction_isChoice:
     5.6  "isAction p \<or> isChoice p"
     5.7 -by (rule process.disc_exhaust) auto
     5.8 +by (rule process.exhaust_disc) auto
     5.9  
    5.10  theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
    5.11  by (cases rule: process.exhaust[of p]) auto
    5.12 @@ -54,7 +54,7 @@
    5.13    Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
    5.14    shows "p = p'"
    5.15    using assms
    5.16 -  by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.disc(3))
    5.17 +  by (coinduct rule: process.coinduct_strong) (metis process.collapse(1,2) process.disc(3))
    5.18  
    5.19  
    5.20  subsection {* Coiteration (unfold) *}
     6.1 --- a/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 15:03:25 2014 +0200
     6.2 +++ b/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 17:19:58 2014 +0200
     6.3 @@ -49,9 +49,9 @@
     6.4    with Step prems show "P a s" by simp
     6.5  qed
     6.6  
     6.7 -lemmas smap_simps[simp] = stream.sel_map
     6.8 -lemmas shd_sset = stream.sel_set(1)
     6.9 -lemmas stl_sset = stream.sel_set(2)
    6.10 +lemmas smap_simps[simp] = stream.map_sel
    6.11 +lemmas shd_sset = stream.set_sel(1)
    6.12 +lemmas stl_sset = stream.set_sel(2)
    6.13  
    6.14  (* only for the non-mutual case: *)
    6.15  theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]:
     7.1 --- a/src/HOL/Bali/Basis.thy	Mon Aug 18 15:03:25 2014 +0200
     7.2 +++ b/src/HOL/Bali/Basis.thy	Mon Aug 18 17:19:58 2014 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4  
     7.5  declare split_if_asm  [split] option.split [split] option.split_asm [split]
     7.6  setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     7.7 -declare if_weak_cong [cong del] option.weak_case_cong [cong del]
     7.8 +declare if_weak_cong [cong del] option.case_cong_weak [cong del]
     7.9  declare length_Suc_conv [iff]
    7.10  
    7.11  lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
     8.1 --- a/src/HOL/Bali/Conform.thy	Mon Aug 18 15:03:25 2014 +0200
     8.2 +++ b/src/HOL/Bali/Conform.thy	Mon Aug 18 17:19:58 2014 +0200
     8.3 @@ -521,7 +521,7 @@
     8.4  apply auto
     8.5  apply (simp only: obj_ty_cong) 
     8.6  apply (force dest: conforms_globsD intro!: lconf_upd 
     8.7 -       simp add: oconf_def cong del: sum.weak_case_cong)
     8.8 +       simp add: oconf_def cong del: sum.case_cong_weak)
     8.9  done
    8.10  
    8.11  lemma conforms_set_locals: 
     9.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Aug 18 15:03:25 2014 +0200
     9.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Aug 18 17:19:58 2014 +0200
     9.3 @@ -1754,7 +1754,7 @@
     9.4    Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
     9.5    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
     9.6    compare.simps compare.exhaust compare.induct compare.rec compare.simps
     9.7 -  compare.size compare.case_cong compare.weak_case_cong compare.case
     9.8 +  compare.size compare.case_cong compare.case_cong_weak compare.case
     9.9    compare.nchotomy compare.split compare.split_asm rec_compare_def
    9.10    compare.eq.refl compare.eq.simps
    9.11    compare.EQ_def compare.GT_def compare.LT_def
    10.1 --- a/src/HOL/Nat.thy	Mon Aug 18 15:03:25 2014 +0200
    10.2 +++ b/src/HOL/Nat.thy	Mon Aug 18 17:19:58 2014 +0200
    10.3 @@ -132,9 +132,9 @@
    10.4    nat.collapse
    10.5    nat.expand
    10.6    nat.sel
    10.7 -  nat.sel_exhaust
    10.8 -  nat.sel_split
    10.9 -  nat.sel_split_asm
   10.10 +  nat.exhaust_sel
   10.11 +  nat.split_sel
   10.12 +  nat.split_sel_asm
   10.13  
   10.14  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
   10.15    -- {* for backward compatibility -- names of variables differ *}
    11.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Mon Aug 18 15:03:25 2014 +0200
    11.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Mon Aug 18 17:19:58 2014 +0200
    11.3 @@ -143,7 +143,7 @@
    11.4    apply (induct xs)
    11.5     apply simp
    11.6     apply (case_tac xs)
    11.7 -    apply (simp_all cong del: list.weak_case_cong)
    11.8 +    apply (simp_all cong del: list.case_cong_weak)
    11.9    done
   11.10  
   11.11  lemma nondec_sort: "nondec (sort xs)"
    12.1 --- a/src/HOL/Product_Type.thy	Mon Aug 18 15:03:25 2014 +0200
    12.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 18 17:19:58 2014 +0200
    12.3 @@ -281,7 +281,7 @@
    12.4  setup {* Sign.parent_path *}
    12.5  
    12.6  declare prod.case [nitpick_simp del]
    12.7 -declare prod.weak_case_cong [cong del]
    12.8 +declare prod.case_cong_weak [cong del]
    12.9  
   12.10  
   12.11  subsubsection {* Tuple syntax *}
   12.12 @@ -486,7 +486,7 @@
   12.13  
   12.14  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   12.15    -- {* Prevents simplification of @{term c}: much faster *}
   12.16 -  by (fact prod.weak_case_cong)
   12.17 +  by (fact prod.case_cong_weak)
   12.18  
   12.19  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   12.20    by (simp add: split_eta)
    13.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
    13.3 @@ -99,13 +99,13 @@
    13.4  val EqN = "Eq_";
    13.5  
    13.6  val corec_codeN = "corec_code";
    13.7 -val disc_map_iffN = "disc_map_iff";
    13.8 -val sel_mapN = "sel_map";
    13.9 -val sel_setN = "sel_set";
   13.10 +val map_disc_iffN = "map_disc_iff";
   13.11 +val map_selN = "map_sel";
   13.12  val set_casesN = "set_cases";
   13.13  val set_emptyN = "set_empty";
   13.14  val set_introsN = "set_intros";
   13.15  val set_inductN = "set_induct";
   13.16 +val set_selN = "set_sel";
   13.17  
   13.18  structure Data = Generic_Data
   13.19  (
   13.20 @@ -309,14 +309,14 @@
   13.21    * (thm list list list * Args.src list);
   13.22  
   13.23  fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
   13.24 -    corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs),
   13.25 -    (sel_corecsss, sel_corec_attrs)) =
   13.26 +    corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
   13.27 +    (corec_selsss, corec_sel_attrs)) =
   13.28    ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
   13.29      coinduct_attrs_pair),
   13.30     map (map (Morphism.thm phi)) corecss,
   13.31 -   map (map (Morphism.thm phi)) disc_corecss,
   13.32 -   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
   13.33 -   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
   13.34 +   map (map (Morphism.thm phi)) corec_discss,
   13.35 +   (map (map (Morphism.thm phi)) corec_disc_iffss, corec_disc_iff_attrs),
   13.36 +   (map (map (map (Morphism.thm phi))) corec_selsss, corec_sel_attrs)) : gfp_sugar_thms;
   13.37  
   13.38  val transfer_gfp_sugar_thms =
   13.39    morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
   13.40 @@ -961,7 +961,7 @@
   13.41          val rel_eqs = map rel_eq_of_bnf pre_bnfs;
   13.42          val rel_monos = map rel_mono_of_bnf pre_bnfs;
   13.43          val dtor_coinducts =
   13.44 -          [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
   13.45 +          [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
   13.46        in
   13.47          map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
   13.48        end;
   13.49 @@ -1010,7 +1010,7 @@
   13.50          |> map (map (unfold_thms lthy @{thms case_sum_if}))
   13.51        end;
   13.52  
   13.53 -    val disc_corec_iff_thmss =
   13.54 +    val corec_disc_iff_thmss =
   13.55        let
   13.56          fun mk_goal c cps gcorec n k disc =
   13.57            mk_Trueprop_eq (disc $ (gcorec $ c),
   13.58 @@ -1023,7 +1023,7 @@
   13.59  
   13.60          val case_splitss' = map (map mk_case_split') cpss;
   13.61  
   13.62 -        val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
   13.63 +        val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
   13.64  
   13.65          fun prove goal tac =
   13.66            Goal.prove_sorry lthy [] [] goal (tac o #context)
   13.67 @@ -1037,11 +1037,11 @@
   13.68          map2 proves goalss tacss
   13.69        end;
   13.70  
   13.71 -    fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs);
   13.72 +    fun mk_corec_disc_thms corecs discIs = map (op RS) (corecs ~~ discIs);
   13.73  
   13.74 -    val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
   13.75 +    val corec_disc_thmss = map2 mk_corec_disc_thms corec_thmss discIss;
   13.76  
   13.77 -    fun mk_sel_corec_thm corec_thm sel sel_thm =
   13.78 +    fun mk_corec_sel_thm corec_thm sel sel_thm =
   13.79        let
   13.80          val (domT, ranT) = dest_funT (fastype_of sel);
   13.81          val arg_cong' =
   13.82 @@ -1053,17 +1053,17 @@
   13.83          corec_thm RS arg_cong' RS sel_thm'
   13.84        end;
   13.85  
   13.86 -    fun mk_sel_corec_thms corec_thmss =
   13.87 -      map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
   13.88 +    fun mk_corec_sel_thms corec_thmss =
   13.89 +      map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
   13.90  
   13.91 -    val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
   13.92 +    val corec_sel_thmsss = mk_corec_sel_thms corec_thmss;
   13.93    in
   13.94      ((coinduct_thms_pairs,
   13.95        mk_coinduct_attributes fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss),
   13.96       corec_thmss,
   13.97 -     disc_corec_thmss,
   13.98 -     (disc_corec_iff_thmss, simp_attrs),
   13.99 -     (sel_corec_thmsss, simp_attrs))
  13.100 +     corec_disc_thmss,
  13.101 +     (corec_disc_iff_thmss, simp_attrs),
  13.102 +     (corec_sel_thmsss, simp_attrs))
  13.103    end;
  13.104  
  13.105  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
  13.106 @@ -1498,7 +1498,7 @@
  13.107                  map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
  13.108                    rel_inject_thms ms;
  13.109  
  13.110 -              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
  13.111 +              val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
  13.112                     (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
  13.113                  let
  13.114                    val live_AsBs = filter (op <>) (As ~~ Bs);
  13.115 @@ -1702,7 +1702,7 @@
  13.116                        (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
  13.117                      end;
  13.118  
  13.119 -                  val disc_map_iff_thms =
  13.120 +                  val map_disc_iff_thms =
  13.121                      let
  13.122                        val discsB = map (mk_disc_or_sel Bs) discs;
  13.123                        val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs;
  13.124 @@ -1721,14 +1721,14 @@
  13.125                        else
  13.126                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
  13.127                            (fn {context = ctxt, prems = _} =>
  13.128 -                            mk_disc_map_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.129 +                            mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.130                                map_thms)
  13.131                          |> Conjunction.elim_balanced (length goals)
  13.132                          |> Proof_Context.export names_lthy lthy
  13.133                          |> map Thm.close_derivation
  13.134                      end;
  13.135  
  13.136 -                  val sel_map_thms =
  13.137 +                  val map_sel_thms =
  13.138                      let
  13.139                        fun mk_goal (discA, selA) =
  13.140                          let
  13.141 @@ -1755,14 +1755,14 @@
  13.142                        else
  13.143                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
  13.144                            (fn {context = ctxt, prems = _} =>
  13.145 -                            mk_sel_map_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.146 +                            mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.147                                map_thms (flat sel_thmss))
  13.148                          |> Conjunction.elim_balanced (length goals)
  13.149                          |> Proof_Context.export names_lthy lthy
  13.150                          |> map Thm.close_derivation
  13.151                      end;
  13.152  
  13.153 -                  val sel_set_thms =
  13.154 +                  val set_sel_thms =
  13.155                      let
  13.156                        fun mk_goal discA selA setA ctxt =
  13.157                          let
  13.158 @@ -1819,14 +1819,14 @@
  13.159                        else
  13.160                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
  13.161                            (fn {context = ctxt, prems = _} =>
  13.162 -                             mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.163 +                             mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
  13.164                                 (flat sel_thmss) set0_thms)
  13.165                          |> Conjunction.elim_balanced (length goals)
  13.166                          |> Proof_Context.export names_lthy lthy
  13.167                          |> map Thm.close_derivation
  13.168                      end;
  13.169                  in
  13.170 -                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
  13.171 +                  (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
  13.172                      (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
  13.173                  end;
  13.174  
  13.175 @@ -1836,19 +1836,19 @@
  13.176                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
  13.177  
  13.178                val notes =
  13.179 -                [(disc_map_iffN, disc_map_iff_thms, K simp_attrs),
  13.180 -                 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
  13.181 +                [(mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
  13.182 +                 (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
  13.183 +                 (map_selN, map_sel_thms, K []),
  13.184                   (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
  13.185                   (rel_distinctN, rel_distinct_thms, K simp_attrs),
  13.186                   (rel_injectN, rel_inject_thms, K simp_attrs),
  13.187                   (rel_introsN, rel_intro_thms, K []),
  13.188                   (rel_selN, rel_sel_thms, K []),
  13.189                   (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
  13.190 -                 (sel_mapN, sel_map_thms, K []),
  13.191 -                 (sel_setN, sel_set_thms, K []),
  13.192                   (set_casesN, set_cases_thms, nth set_cases_attrss),
  13.193                   (set_emptyN, set_empty_thms, K []),
  13.194 -                 (set_introsN, set_intros_thms, K [])]
  13.195 +                 (set_introsN, set_intros_thms, K []),
  13.196 +                 (set_selN, set_sel_thms, K [])]
  13.197                  |> massage_simple_notes fp_b_name;
  13.198  
  13.199                val (noted, lthy') =
  13.200 @@ -1948,10 +1948,10 @@
  13.201          ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
  13.202            (corecs, corec_defs)), lthy) =
  13.203        let
  13.204 -        val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
  13.205 +        val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
  13.206                (coinduct_attrs, common_coinduct_attrs)),
  13.207 -             corec_thmss, disc_corec_thmss,
  13.208 -             (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
  13.209 +             corec_thmss, corec_disc_thmss,
  13.210 +             (corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) =
  13.211            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
  13.212              dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
  13.213              ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
  13.214 @@ -1969,7 +1969,7 @@
  13.215                    [thm, eq_ifIN ctxt thms]));
  13.216  
  13.217          val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
  13.218 -        val sel_corec_thmss = map flat sel_corec_thmsss;
  13.219 +        val corec_sel_thmss = map flat corec_sel_thmsss;
  13.220  
  13.221          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
  13.222          val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
  13.223 @@ -2001,39 +2001,39 @@
  13.224  
  13.225          val simp_thmss =
  13.226            map6 mk_simp_thms ctr_sugars
  13.227 -            (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
  13.228 +            (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
  13.229              mapss rel_injectss rel_distinctss setss;
  13.230  
  13.231          val common_notes =
  13.232            (set_inductN, set_induct_thms, nth set_induct_attrss) ::
  13.233            (if nn > 1 then
  13.234              [(coinductN, [coinduct_thm], K common_coinduct_attrs),
  13.235 -             (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs),
  13.236 -             (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)]
  13.237 +             (coinduct_strongN, [coinduct_strong_thm], K common_coinduct_attrs),
  13.238 +             (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs)]
  13.239             else [])
  13.240            |> massage_simple_notes fp_common_name;
  13.241  
  13.242          val notes =
  13.243            [(coinductN, map single coinduct_thms,
  13.244              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
  13.245 +           (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
  13.246             (corecN, corec_thmss, K []),
  13.247             (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
  13.248 -           (disc_corecN, disc_corec_thmss, K []),
  13.249 -           (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
  13.250 +           (corec_discN, corec_disc_thmss, K []),
  13.251 +           (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
  13.252 +           (corec_selN, corec_sel_thmss, K corec_sel_attrs),
  13.253             (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
  13.254 -           (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
  13.255 -           (simpsN, simp_thmss, K []),
  13.256 -           (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
  13.257 +           (simpsN, simp_thmss, K [])]
  13.258            |> massage_multi_notes;
  13.259        in
  13.260          lthy
  13.261          |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
  13.262 -          [flat sel_corec_thmss, flat corec_thmss]
  13.263 +          [flat corec_sel_thmss, flat corec_thmss]
  13.264          |> Local_Theory.notes (common_notes @ notes)
  13.265          |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
  13.266            live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
  13.267 -          [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
  13.268 -          corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
  13.269 +          [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms])
  13.270 +          corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss
  13.271        end;
  13.272  
  13.273      val lthy'' = lthy'
    14.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
    14.3 @@ -17,15 +17,16 @@
    14.4      thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
    14.5      thm list list list -> tactic
    14.6    val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
    14.7 +  val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    14.8    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    14.9      tactic
   14.10 -  val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
   14.11 -  val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   14.12    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   14.13    val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
   14.14    val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
   14.15      thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   14.16    val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
   14.17 +  val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   14.18 +  val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
   14.19    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
   14.20      tactic
   14.21    val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
   14.22 @@ -37,13 +38,12 @@
   14.23      thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
   14.24    val mk_rel_sel_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
   14.25      thm list -> thm list -> tactic
   14.26 -  val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
   14.27 -  val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
   14.28    val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
   14.29    val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   14.30    val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
   14.31      thm list -> thm list -> thm list -> thm list -> tactic
   14.32    val mk_set_intros_tac: Proof.context -> thm list -> tactic
   14.33 +  val mk_set_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
   14.34  end;
   14.35  
   14.36  structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
   14.37 @@ -126,22 +126,13 @@
   14.38      HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
   14.39    end;
   14.40  
   14.41 -fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
   14.42 +fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
   14.43    EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
   14.44        HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
   14.45        HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
   14.46        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
   14.47      (map rtac case_splits' @ [K all_tac]) corecs discs);
   14.48  
   14.49 -fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
   14.50 -  TRYALL Goal.conjunction_tac THEN
   14.51 -  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
   14.52 -    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   14.53 -  unfold_thms_tac ctxt maps THEN
   14.54 -  unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
   14.55 -    handle THM _ => thm RS eqTrueI) discs) THEN
   14.56 -  ALLGOALS (rtac refl ORELSE' rtac TrueI);
   14.57 -
   14.58  fun solve_prem_prem_tac ctxt =
   14.59    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
   14.60      hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   14.61 @@ -221,6 +212,25 @@
   14.62        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
   14.63        selsss));
   14.64  
   14.65 +fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
   14.66 +  TRYALL Goal.conjunction_tac THEN
   14.67 +  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
   14.68 +    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   14.69 +  unfold_thms_tac ctxt maps THEN
   14.70 +  unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
   14.71 +    handle THM _ => thm RS eqTrueI) discs) THEN
   14.72 +  ALLGOALS (rtac refl ORELSE' rtac TrueI);
   14.73 +
   14.74 +fun mk_map_sel_tac ctxt ct exhaust discs maps sels =
   14.75 +  TRYALL Goal.conjunction_tac THEN
   14.76 +    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
   14.77 +      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   14.78 +    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
   14.79 +      @{thms not_True_eq_False not_False_eq_True}) THEN
   14.80 +    TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
   14.81 +    unfold_thms_tac ctxt (maps @ sels) THEN
   14.82 +    ALLGOALS (rtac refl);
   14.83 +
   14.84  fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
   14.85    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
   14.86      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
   14.87 @@ -280,17 +290,7 @@
   14.88      (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
   14.89    TRYALL (resolve_tac [TrueI, refl]);
   14.90  
   14.91 -fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
   14.92 -  TRYALL Goal.conjunction_tac THEN
   14.93 -    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
   14.94 -      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   14.95 -    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
   14.96 -      @{thms not_True_eq_False not_False_eq_True}) THEN
   14.97 -    TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
   14.98 -    unfold_thms_tac ctxt (maps @ sels) THEN
   14.99 -    ALLGOALS (rtac refl);
  14.100 -
  14.101 -fun mk_sel_set_tac ctxt ct exhaust discs sels sets =
  14.102 +fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
  14.103    TRYALL Goal.conjunction_tac THEN
  14.104      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
  14.105        REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    15.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
    15.3 @@ -257,7 +257,7 @@
    15.4              fp_bs xtor_co_recs lthy
    15.5            |>> split_list;
    15.6  
    15.7 -        val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
    15.8 +        val ((common_co_inducts, co_inductss, co_rec_thmss, corec_disc_thmss, corec_sel_thmsss),
    15.9               fp_sugar_thms) =
   15.10            if fp = Least_FP then
   15.11              derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
   15.12 @@ -272,30 +272,30 @@
   15.13                dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
   15.14                mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
   15.15                ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
   15.16 -            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, disc_corec_thmss, _,
   15.17 -                     (sel_corec_thmsss, _)) =>
   15.18 +            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
   15.19 +                     (corec_sel_thmsss, _)) =>
   15.20                (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
   15.21 -               disc_corec_thmss, sel_corec_thmsss))
   15.22 +               corec_disc_thmss, corec_sel_thmsss))
   15.23              ||> (fn info => (NONE, SOME info));
   15.24  
   15.25          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   15.26  
   15.27          fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
   15.28 -            co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
   15.29 +            co_rec_def maps co_inducts co_rec_thms corec_disc_thms corec_sel_thmss
   15.30              ({rel_injects, rel_distincts, ...} : fp_sugar) =
   15.31            {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
   15.32             fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
   15.33             fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
   15.34             ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
   15.35             co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
   15.36 -           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
   15.37 -           sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
   15.38 +           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = corec_disc_thms,
   15.39 +           sel_co_recss = corec_sel_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
   15.40            |> morph_fp_sugar phi;
   15.41  
   15.42          val target_fp_sugars =
   15.43            map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
   15.44 -            co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
   15.45 -            sel_corec_thmsss fp_sugars0;
   15.46 +            co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss corec_disc_thmss
   15.47 +            corec_sel_thmsss fp_sugars0;
   15.48  
   15.49          val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
   15.50        in
    16.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Aug 18 15:03:25 2014 +0200
    16.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Aug 18 17:19:58 2014 +0200
    16.3 @@ -71,7 +71,10 @@
    16.4    val caseN: string
    16.5    val coN: string
    16.6    val coinductN: string
    16.7 +  val coinduct_strongN: string
    16.8    val corecN: string
    16.9 +  val corec_discN: string
   16.10 +  val corec_disc_iffN: string
   16.11    val ctorN: string
   16.12    val ctor_dtorN: string
   16.13    val ctor_exhaustN: string
   16.14 @@ -91,8 +94,6 @@
   16.15    val ctor_rel_inductN: string
   16.16    val ctor_set_inclN: string
   16.17    val ctor_set_set_inclN: string
   16.18 -  val disc_corecN: string
   16.19 -  val disc_corec_iffN: string
   16.20    val dtorN: string
   16.21    val dtor_coinductN: string
   16.22    val dtor_corecN: string
   16.23 @@ -103,13 +104,13 @@
   16.24    val dtor_injectN: string
   16.25    val dtor_mapN: string
   16.26    val dtor_map_coinductN: string
   16.27 -  val dtor_map_strong_coinductN: string
   16.28 +  val dtor_map_coinduct_strongN: string
   16.29    val dtor_map_uniqueN: string
   16.30    val dtor_relN: string
   16.31    val dtor_rel_coinductN: string
   16.32    val dtor_set_inclN: string
   16.33    val dtor_set_set_inclN: string
   16.34 -  val dtor_strong_coinductN: string
   16.35 +  val dtor_coinduct_strongN: string
   16.36    val dtor_unfoldN: string
   16.37    val dtor_unfold_o_mapN: string
   16.38    val dtor_unfold_transferN: string
   16.39 @@ -134,14 +135,13 @@
   16.40    val rel_distinctN: string
   16.41    val rel_selN: string
   16.42    val rvN: string
   16.43 -  val sel_corecN: string
   16.44 +  val corec_selN: string
   16.45    val set_inclN: string
   16.46    val set_set_inclN: string
   16.47    val setN: string
   16.48    val simpsN: string
   16.49    val strTN: string
   16.50    val str_initN: string
   16.51 -  val strong_coinductN: string
   16.52    val sum_bdN: string
   16.53    val sum_bdTN: string
   16.54    val uniqueN: string
   16.55 @@ -206,7 +206,7 @@
   16.56    val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
   16.57      thm list -> thm list -> thm list
   16.58  
   16.59 -  val mk_strong_coinduct_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
   16.60 +  val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
   16.61  
   16.62    val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
   16.63        BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
   16.64 @@ -393,9 +393,9 @@
   16.65  val ctor_induct2N = ctor_inductN ^ "2"
   16.66  val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
   16.67  val dtor_coinductN = dtorN ^ "_" ^ coinductN
   16.68 -val strong_coinductN = "strong_" ^ coinductN
   16.69 -val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
   16.70 -val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
   16.71 +val coinduct_strongN = coinductN ^ "_strong"
   16.72 +val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN
   16.73 +val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN
   16.74  val colN = "col"
   16.75  val set_inclN = "set_incl"
   16.76  val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
   16.77 @@ -406,9 +406,9 @@
   16.78  
   16.79  val caseN = "case"
   16.80  val discN = "disc"
   16.81 -val disc_corecN = discN ^ "_" ^ corecN
   16.82 +val corec_discN = corecN ^ "_" ^ discN
   16.83  val iffN = "_iff"
   16.84 -val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
   16.85 +val corec_disc_iffN = corec_discN ^ iffN
   16.86  val distinctN = "distinct"
   16.87  val rel_distinctN = relN ^ "_" ^ distinctN
   16.88  val injectN = "inject"
   16.89 @@ -421,7 +421,7 @@
   16.90  val rel_inductN = relN ^ "_" ^ inductN
   16.91  val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
   16.92  val selN = "sel"
   16.93 -val sel_corecN = selN ^ "_" ^ corecN
   16.94 +val corec_selN = corecN ^ "_" ^ selN
   16.95  
   16.96  fun co_prefix fp = case_fp fp "" "co";
   16.97  
   16.98 @@ -634,7 +634,7 @@
   16.99      split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
  16.100    end;
  16.101  
  16.102 -fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
  16.103 +fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
  16.104    let
  16.105      val n = Thm.nprems_of coind;
  16.106      val m = Thm.nprems_of (hd rel_monos) - n;
    17.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
    17.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
    17.3 @@ -69,15 +69,15 @@
    17.4     calls: corec_call list,
    17.5     discI: thm,
    17.6     sel_thms: thm list,
    17.7 -   disc_excludess: thm list list,
    17.8 +   distinct_discss: thm list list,
    17.9     collapse: thm,
   17.10     corec_thm: thm,
   17.11 -   disc_corec: thm,
   17.12 -   sel_corecs: thm list};
   17.13 +   corec_disc: thm,
   17.14 +   corec_sels: thm list};
   17.15  
   17.16  type corec_spec =
   17.17    {corec: term,
   17.18 -   disc_exhausts: thm list,
   17.19 +   exhaust_discs: thm list,
   17.20     sel_defs: thm list,
   17.21     fp_nesting_maps: thm list,
   17.22     fp_nesting_map_ident0s: thm list,
   17.23 @@ -159,7 +159,7 @@
   17.24              (case fastype_of1 (bound_Ts, nth args n) of
   17.25                Type (s, Ts) =>
   17.26                (case dest_case ctxt s Ts t of
   17.27 -                SOME ({sel_splits = _ :: _, ...}, conds', branches) =>
   17.28 +                SOME ({split_sels = _ :: _, ...}, conds', branches) =>
   17.29                  fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
   17.30                | _ => f conds t)
   17.31              | _ => f conds t)
   17.32 @@ -173,7 +173,7 @@
   17.33  
   17.34  fun case_of ctxt s =
   17.35    (case ctr_sugar_of ctxt s of
   17.36 -    SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
   17.37 +    SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
   17.38    | _ => NONE);
   17.39  
   17.40  fun massage_let_if_case ctxt has_call massage_leaf =
   17.41 @@ -343,8 +343,8 @@
   17.42  
   17.43  fun case_thms_of_term ctxt t =
   17.44    let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
   17.45 -    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars,
   17.46 -     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
   17.47 +    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars,
   17.48 +     maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars)
   17.49    end;
   17.50  
   17.51  fun basic_corec_specs_of ctxt res_T =
   17.52 @@ -444,32 +444,32 @@
   17.53           else No_Corec) g_i
   17.54        | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
   17.55  
   17.56 -    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
   17.57 -        corec_thm disc_corec sel_corecs =
   17.58 +    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse
   17.59 +        corec_thm corec_disc corec_sels =
   17.60        let val nullary = not (can dest_funT (fastype_of ctr)) in
   17.61          {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
   17.62           calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
   17.63 -         disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
   17.64 -         disc_corec = disc_corec, sel_corecs = sel_corecs}
   17.65 +         distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
   17.66 +         corec_disc = corec_disc, corec_sels = corec_sels}
   17.67        end;
   17.68  
   17.69 -    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
   17.70 -        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
   17.71 +    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
   17.72 +        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
   17.73        let val p_ios = map SOME p_is @ [NONE] in
   17.74          map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
   17.75 -          disc_excludesss collapses corec_thms disc_corecs sel_corecss
   17.76 +          distinct_discsss collapses corec_thms corec_discs corec_selss
   17.77        end;
   17.78  
   17.79 -    fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec,
   17.80 -        co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
   17.81 -        sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
   17.82 -      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
   17.83 +    fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
   17.84 +        co_rec_thms = corec_thms, disc_co_recs = corec_discs,
   17.85 +        sel_co_recss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
   17.86 +      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
   17.87         sel_defs = sel_defs,
   17.88         fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
   17.89         fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
   17.90         fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
   17.91 -       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
   17.92 -         sel_corecss};
   17.93 +       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
   17.94 +         corec_selss};
   17.95    in
   17.96      ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   17.97        co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
   17.98 @@ -993,8 +993,8 @@
   17.99        |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
  17.100          (ctr, map (K []) sels))) basic_ctr_specss);
  17.101  
  17.102 -    val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
  17.103 -          strong_coinduct_thms), lthy') =
  17.104 +    val ((n2m, corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms,
  17.105 +          coinduct_strong_thms), lthy') =
  17.106        corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
  17.107      val corec_specs = take actual_nn corec_specs';
  17.108      val ctr_specss = map #ctr_specs corec_specs;
  17.109 @@ -1061,15 +1061,15 @@
  17.110          de_facto_exhaustives disc_eqnss
  17.111        |> list_all_fun_args []
  17.112      val nchotomy_taut_thmss =
  17.113 -      map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} =>
  17.114 +      map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
  17.115            fn {code_rhs_opt, ...} :: _ => fn [] => K []
  17.116              | [goal] => fn true =>
  17.117                let
  17.118 -                val (_, _, arg_disc_exhausts, _, _) =
  17.119 +                val (_, _, arg_exhaust_discs, _, _) =
  17.120                    case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
  17.121                in
  17.122                  [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
  17.123 -                   mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts))
  17.124 +                   mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
  17.125                   |> Thm.close_derivation]
  17.126                end
  17.127              | false =>
  17.128 @@ -1133,7 +1133,7 @@
  17.129              []
  17.130            else
  17.131              let
  17.132 -              val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
  17.133 +              val {disc, corec_disc, ...} = nth ctr_specs ctr_no;
  17.134                val k = 1 + ctr_no;
  17.135                val m = length prems;
  17.136                val goal =
  17.137 @@ -1146,7 +1146,7 @@
  17.138                if prems = [@{term False}] then
  17.139                  []
  17.140                else
  17.141 -                mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
  17.142 +                mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
  17.143                  |> K |> Goal.prove_sorry lthy [] [] goal
  17.144                  |> Thm.close_derivation
  17.145                  |> pair (#disc (nth ctr_specs ctr_no))
  17.146 @@ -1163,8 +1163,8 @@
  17.147              val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
  17.148              val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
  17.149                (find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
  17.150 -            val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec)
  17.151 -              |> nth (#sel_corecs ctr_spec);
  17.152 +            val corec_sel = find_index (curry (op =) sel) (#sels ctr_spec)
  17.153 +              |> nth (#corec_sels ctr_spec);
  17.154              val k = 1 + ctr_no;
  17.155              val m = length prems;
  17.156              val goal =
  17.157 @@ -1174,10 +1174,10 @@
  17.158                |> HOLogic.mk_Trueprop o HOLogic.mk_eq
  17.159                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
  17.160                |> curry Logic.list_all (map dest_Free fun_args);
  17.161 -            val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
  17.162 +            val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term;
  17.163            in
  17.164 -            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
  17.165 -              fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss
  17.166 +            mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps
  17.167 +              fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss
  17.168              |> K |> Goal.prove_sorry lthy [] [] goal
  17.169              |> Thm.close_derivation
  17.170              |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
  17.171 @@ -1306,16 +1306,16 @@
  17.172                      val (raw_goal, goal) = (raw_rhs, rhs)
  17.173                        |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
  17.174                          #> curry Logic.list_all (map dest_Free fun_args));
  17.175 -                    val (distincts, discIs, _, sel_splits, sel_split_asms) =
  17.176 +                    val (distincts, discIs, _, split_sels, split_sel_asms) =
  17.177                        case_thms_of_term lthy raw_rhs;
  17.178  
  17.179 -                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
  17.180 -                        sel_split_asms ms ctr_thms
  17.181 +                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels
  17.182 +                        split_sel_asms ms ctr_thms
  17.183                          (if exhaustive_code then try the_single nchotomys else NONE)
  17.184                        |> K |> Goal.prove_sorry lthy [] [] raw_goal
  17.185                        |> Thm.close_derivation;
  17.186                    in
  17.187 -                    mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
  17.188 +                    mk_primcorec_code_tac lthy distincts split_sels raw_code_thm
  17.189                      |> K |> Goal.prove_sorry lthy [] [] goal
  17.190                      |> Thm.close_derivation
  17.191                      |> single
  17.192 @@ -1337,14 +1337,14 @@
  17.193              []
  17.194            else
  17.195              let
  17.196 -              val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
  17.197 +              val {disc, distinct_discss, ...} = nth ctr_specs ctr_no;
  17.198                val goal =
  17.199                  mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
  17.200                    mk_conjs prems)
  17.201                  |> curry Logic.list_all (map dest_Free fun_args);
  17.202              in
  17.203                mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
  17.204 -                (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
  17.205 +                (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
  17.206                |> K |> Goal.prove_sorry lthy [] [] goal
  17.207                |> Thm.close_derivation
  17.208                |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
  17.209 @@ -1385,7 +1385,7 @@
  17.210             (exhaustN, nontriv_exhaust_thmss, []),
  17.211             (selN, sel_thmss, simp_attrs),
  17.212             (simpsN, simp_thmss, []),
  17.213 -           (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
  17.214 +           (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, [])]
  17.215            |> maps (fn (thmN, thmss, attrs) =>
  17.216              map2 (fn fun_name => fn thms =>
  17.217                  ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
  17.218 @@ -1394,7 +1394,7 @@
  17.219  
  17.220          val common_notes =
  17.221            [(coinductN, if n2m then [coinduct_thm] else [], []),
  17.222 -           (strong_coinductN, if n2m then [strong_coinduct_thm] else [], [])]
  17.223 +           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], [])]
  17.224            |> filter_out (null o #2)
  17.225            |> map (fn (thmN, thms, attrs) =>
  17.226              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
    18.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
    18.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
    18.3 @@ -54,8 +54,8 @@
    18.4  fun distinct_in_prems_tac distincts =
    18.5    eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
    18.6  
    18.7 -fun mk_primcorec_nchotomy_tac ctxt disc_exhausts =
    18.8 -  HEADGOAL (Method.insert_tac disc_exhausts THEN' clean_blast_tac ctxt);
    18.9 +fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
   18.10 +  HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
   18.11  
   18.12  fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
   18.13    let val ks = 1 upto n in
   18.14 @@ -105,11 +105,11 @@
   18.15  fun prelude_tac ctxt defs thm =
   18.16    unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
   18.17  
   18.18 -fun mk_primcorec_disc_tac ctxt defs disc_corec k m excludesss =
   18.19 -  prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m excludesss;
   18.20 +fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
   18.21 +  prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
   18.22  
   18.23  fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
   18.24 -    disc_excludes =
   18.25 +    distinct_discs =
   18.26    HEADGOAL (rtac iffI THEN'
   18.27      rtac fun_exhaust THEN'
   18.28      K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
   18.29 @@ -121,7 +121,7 @@
   18.30              rtac FalseE THEN'
   18.31              (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
   18.32               cut_tac fun_disc') THEN'
   18.33 -            dresolve_tac disc_excludes THEN' etac notE THEN' atac)
   18.34 +            dresolve_tac distinct_discs THEN' etac notE THEN' atac)
   18.35        fun_discss) THEN'
   18.36      (etac FalseE ORELSE'
   18.37       resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
    19.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
    19.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
    19.3 @@ -103,7 +103,7 @@
    19.4  val ord_eq_le_trans = @{thm ord_eq_le_trans};
    19.5  val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
    19.6  val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
    19.7 -val sum_weak_case_cong = @{thm sum.weak_case_cong};
    19.8 +val sum_case_cong_weak = @{thm sum.case_cong_weak};
    19.9  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
   19.10  val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
   19.11  val rev_bspec = Drule.rotate_prems 1 bspec;
   19.12 @@ -430,7 +430,7 @@
   19.13          CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   19.14            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
   19.15              rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
   19.16 -            if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
   19.17 +            if n = 1 then K all_tac else etac (sum_case_cong_weak RS trans),
   19.18              rtac (mk_sum_caseN n i RS trans), atac])
   19.19            ks])
   19.20          rv_Conss)
   19.21 @@ -565,7 +565,7 @@
   19.22                rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
   19.23                rtac exI, rtac conjI,
   19.24                if n = 1 then rtac refl
   19.25 -              else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
   19.26 +              else etac (sum_case_cong_weak RS trans) THEN' rtac (mk_sum_caseN n i),
   19.27                CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
   19.28                  EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
   19.29                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   19.30 @@ -603,7 +603,7 @@
   19.31          CONVERSION (Conv.top_conv
   19.32            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   19.33          if n = 1 then K all_tac
   19.34 -        else (rtac (sum_weak_case_cong RS trans) THEN'
   19.35 +        else (rtac (sum_case_cong_weak RS trans) THEN'
   19.36            rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
   19.37          rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
   19.38          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
   19.39 @@ -628,7 +628,7 @@
   19.40              CONVERSION (Conv.top_conv
   19.41                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
   19.42              if n = 1 then K all_tac
   19.43 -            else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
   19.44 +            else rtac sum_case_cong_weak THEN' rtac (mk_sum_caseN n i' RS trans),
   19.45              SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl])
   19.46          ks to_sbd_injs from_to_sbds)];
   19.47    in
    20.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Aug 18 15:03:25 2014 +0200
    20.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Aug 18 17:19:58 2014 +0200
    20.3 @@ -138,12 +138,12 @@
    20.4      val inducts = map (the_single o #co_inducts) fp_sugars;
    20.5  
    20.6      fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
    20.7 -        distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
    20.8 +        distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
    20.9        (T_name0,
   20.10         {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
   20.11          inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
   20.12          rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
   20.13 -        case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
   20.14 +        case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
   20.15          split_asm = split_asm});
   20.16  
   20.17      val infos = map_index mk_info (take nn_fp fp_sugars);
    21.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
    21.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
    21.3 @@ -18,7 +18,7 @@
    21.4       distincts: thm list,
    21.5       case_thms: thm list,
    21.6       case_cong: thm,
    21.7 -     weak_case_cong: thm,
    21.8 +     case_cong_weak: thm,
    21.9       split: thm,
   21.10       split_asm: thm,
   21.11       disc_defs: thm list,
   21.12 @@ -26,13 +26,13 @@
   21.13       discIs: thm list,
   21.14       sel_defs: thm list,
   21.15       sel_thmss: thm list list,
   21.16 -     disc_excludesss: thm list list list,
   21.17 -     disc_exhausts: thm list,
   21.18 -     sel_exhausts: thm list,
   21.19 +     distinct_discsss: thm list list list,
   21.20 +     exhaust_discs: thm list,
   21.21 +     exhaust_sels: thm list,
   21.22       collapses: thm list,
   21.23       expands: thm list,
   21.24 -     sel_splits: thm list,
   21.25 -     sel_split_asms: thm list,
   21.26 +     split_sels: thm list,
   21.27 +     split_sel_asms: thm list,
   21.28       case_eq_ifs: thm list};
   21.29  
   21.30    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
   21.31 @@ -90,7 +90,7 @@
   21.32     distincts: thm list,
   21.33     case_thms: thm list,
   21.34     case_cong: thm,
   21.35 -   weak_case_cong: thm,
   21.36 +   case_cong_weak: thm,
   21.37     split: thm,
   21.38     split_asm: thm,
   21.39     disc_defs: thm list,
   21.40 @@ -98,19 +98,19 @@
   21.41     discIs: thm list,
   21.42     sel_defs: thm list,
   21.43     sel_thmss: thm list list,
   21.44 -   disc_excludesss: thm list list list,
   21.45 -   disc_exhausts: thm list,
   21.46 -   sel_exhausts: thm list,
   21.47 +   distinct_discsss: thm list list list,
   21.48 +   exhaust_discs: thm list,
   21.49 +   exhaust_sels: thm list,
   21.50     collapses: thm list,
   21.51     expands: thm list,
   21.52 -   sel_splits: thm list,
   21.53 -   sel_split_asms: thm list,
   21.54 +   split_sels: thm list,
   21.55 +   split_sel_asms: thm list,
   21.56     case_eq_ifs: thm list};
   21.57  
   21.58  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
   21.59 -    case_thms, case_cong, weak_case_cong, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
   21.60 -    sel_thmss, disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits,
   21.61 -    sel_split_asms, case_eq_ifs} =
   21.62 +    case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
   21.63 +    sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
   21.64 +    split_sel_asms, case_eq_ifs} =
   21.65    {ctrs = map (Morphism.term phi) ctrs,
   21.66     casex = Morphism.term phi casex,
   21.67     discs = map (Morphism.term phi) discs,
   21.68 @@ -121,7 +121,7 @@
   21.69     distincts = map (Morphism.thm phi) distincts,
   21.70     case_thms = map (Morphism.thm phi) case_thms,
   21.71     case_cong = Morphism.thm phi case_cong,
   21.72 -   weak_case_cong = Morphism.thm phi weak_case_cong,
   21.73 +   case_cong_weak = Morphism.thm phi case_cong_weak,
   21.74     split = Morphism.thm phi split,
   21.75     split_asm = Morphism.thm phi split_asm,
   21.76     disc_defs = map (Morphism.thm phi) disc_defs,
   21.77 @@ -129,13 +129,13 @@
   21.78     discIs = map (Morphism.thm phi) discIs,
   21.79     sel_defs = map (Morphism.thm phi) sel_defs,
   21.80     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
   21.81 -   disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
   21.82 -   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
   21.83 -   sel_exhausts = map (Morphism.thm phi) sel_exhausts,
   21.84 +   distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss,
   21.85 +   exhaust_discs = map (Morphism.thm phi) exhaust_discs,
   21.86 +   exhaust_sels = map (Morphism.thm phi) exhaust_sels,
   21.87     collapses = map (Morphism.thm phi) collapses,
   21.88     expands = map (Morphism.thm phi) expands,
   21.89 -   sel_splits = map (Morphism.thm phi) sel_splits,
   21.90 -   sel_split_asms = map (Morphism.thm phi) sel_split_asms,
   21.91 +   split_sels = map (Morphism.thm phi) split_sels,
   21.92 +   split_sel_asms = map (Morphism.thm phi) split_sel_asms,
   21.93     case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
   21.94  
   21.95  val transfer_ctr_sugar =
   21.96 @@ -200,23 +200,23 @@
   21.97  val case_congN = "case_cong";
   21.98  val case_eq_ifN = "case_eq_if";
   21.99  val collapseN = "collapse";
  21.100 -val disc_excludeN = "disc_exclude";
  21.101 -val disc_exhaustN = "disc_exhaust";
  21.102  val discN = "disc";
  21.103  val discIN = "discI";
  21.104  val distinctN = "distinct";
  21.105 +val distinct_discN = "distinct_disc";
  21.106  val exhaustN = "exhaust";
  21.107 +val exhaust_discN = "exhaust_disc";
  21.108  val expandN = "expand";
  21.109  val injectN = "inject";
  21.110  val nchotomyN = "nchotomy";
  21.111  val selN = "sel";
  21.112 -val sel_exhaustN = "sel_exhaust";
  21.113 -val sel_splitN = "sel_split";
  21.114 -val sel_split_asmN = "sel_split_asm";
  21.115 +val exhaust_selN = "exhaust_sel";
  21.116  val splitN = "split";
  21.117 +val split_asmN = "split_asm";
  21.118 +val split_selN = "split_sel";
  21.119 +val split_sel_asmN = "split_sel_asm";
  21.120  val splitsN = "splits";
  21.121 -val split_asmN = "split_asm";
  21.122 -val weak_case_cong_thmsN = "weak_case_cong";
  21.123 +val case_cong_weak_thmsN = "case_cong_weak";
  21.124  
  21.125  val cong_attrs = @{attributes [cong]};
  21.126  val dest_attrs = @{attributes [dest]};
  21.127 @@ -677,7 +677,7 @@
  21.128                ks goals inject_thmss distinct_thmsss
  21.129            end;
  21.130  
  21.131 -        val (case_cong_thm, weak_case_cong_thm) =
  21.132 +        val (case_cong_thm, case_cong_weak_thm) =
  21.133            let
  21.134              fun mk_prem xctr xs xf xg =
  21.135                fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
  21.136 @@ -733,9 +733,9 @@
  21.137            end;
  21.138  
  21.139          val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
  21.140 -             discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
  21.141 -             disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, safe_collapse_thms,
  21.142 -             expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
  21.143 +             discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
  21.144 +             exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
  21.145 +             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) =
  21.146            if no_discs_sels then
  21.147              ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
  21.148            else
  21.149 @@ -827,7 +827,7 @@
  21.150                  flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
  21.151                    discI_thms);
  21.152  
  21.153 -              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
  21.154 +              val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) =
  21.155                  let
  21.156                    fun mk_goal [] = []
  21.157                      | mk_goal [((_, udisc), (_, udisc'))] =
  21.158 @@ -843,25 +843,25 @@
  21.159                    val half_goalss = map mk_goal half_pairss;
  21.160                    val half_thmss =
  21.161                      map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
  21.162 -                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
  21.163 +                        fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal])
  21.164                        half_goalss half_pairss (flat disc_thmss');
  21.165  
  21.166                    val other_half_goalss = map (mk_goal o map swap) half_pairss;
  21.167                    val other_half_thmss =
  21.168 -                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
  21.169 +                    map2 (map2 (prove o mk_other_half_distinct_disc_tac)) half_thmss
  21.170                        other_half_goalss;
  21.171                  in
  21.172                    join_halves n half_thmss other_half_thmss ||> `transpose
  21.173                    |>> has_alternate_disc_def ? K []
  21.174                  end;
  21.175  
  21.176 -              val disc_exhaust_thm =
  21.177 +              val exhaust_disc_thm =
  21.178                  let
  21.179                    fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
  21.180                    val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
  21.181                  in
  21.182                    Goal.prove_sorry lthy [] [] goal (fn _ =>
  21.183 -                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
  21.184 +                    mk_exhaust_disc_tac n exhaust_thm discI_thms)
  21.185                    |> Thm.close_derivation
  21.186                  end;
  21.187  
  21.188 @@ -890,13 +890,13 @@
  21.189                val swapped_all_collapse_thms =
  21.190                  map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms;
  21.191  
  21.192 -              val sel_exhaust_thm =
  21.193 +              val exhaust_sel_thm =
  21.194                  let
  21.195                    fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)];
  21.196                    val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs));
  21.197                  in
  21.198                    Goal.prove_sorry lthy [] [] goal (fn _ =>
  21.199 -                    mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms)
  21.200 +                    mk_exhaust_sel_tac n exhaust_disc_thm swapped_all_collapse_thms)
  21.201                    |> Thm.close_derivation
  21.202                  end;
  21.203  
  21.204 @@ -919,14 +919,14 @@
  21.205                      map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
  21.206                  in
  21.207                    Goal.prove_sorry lthy [] [] goal (fn _ =>
  21.208 -                    mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
  21.209 -                      (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
  21.210 -                      disc_exclude_thmsss')
  21.211 +                    mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm)
  21.212 +                      (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
  21.213 +                      distinct_disc_thmsss')
  21.214                    |> singleton (Proof_Context.export names_lthy lthy)
  21.215                    |> Thm.close_derivation
  21.216                  end;
  21.217  
  21.218 -              val (sel_split_thm, sel_split_asm_thm) =
  21.219 +              val (split_sel_thm, split_sel_asm_thm) =
  21.220                  let
  21.221                    val zss = map (K []) xss;
  21.222                    val goal = mk_split_goal usel_ctrs zss usel_fs;
  21.223 @@ -949,9 +949,9 @@
  21.224                  end;
  21.225              in
  21.226                (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
  21.227 -               discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss,
  21.228 -               [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms,
  21.229 -               [expand_thm], [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
  21.230 +               discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
  21.231 +               [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
  21.232 +               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm])
  21.233              end;
  21.234  
  21.235          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
  21.236 @@ -966,30 +966,28 @@
  21.237             (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
  21.238            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
  21.239  
  21.240 -        (* "exhaust" is deliberately put first to avoid apparent circular dependencies in the proof
  21.241 -           objects, which would confuse MaSh. *)
  21.242          val notes =
  21.243 -          [(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
  21.244 -           (caseN, case_thms, code_nitpicksimp_simp_attrs),
  21.245 +          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
  21.246             (case_congN, [case_cong_thm], []),
  21.247 +           (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
  21.248             (case_eq_ifN, case_eq_if_thms, []),
  21.249             (collapseN, safe_collapse_thms, simp_attrs),
  21.250             (discN, flat nontriv_disc_thmss, simp_attrs),
  21.251             (discIN, nontriv_discI_thms, []),
  21.252 -           (disc_excludeN, disc_exclude_thms, dest_attrs),
  21.253 -           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
  21.254             (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
  21.255 +           (distinct_discN, distinct_disc_thms, dest_attrs),
  21.256 +           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
  21.257 +           (exhaust_discN, exhaust_disc_thms, [exhaust_case_names_attr]),
  21.258 +           (exhaust_selN, exhaust_sel_thms, [exhaust_case_names_attr]),
  21.259             (expandN, expand_thms, []),
  21.260             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
  21.261             (nchotomyN, [nchotomy_thm], []),
  21.262             (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
  21.263 -           (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
  21.264 -           (sel_splitN, sel_split_thms, []),
  21.265 -           (sel_split_asmN, sel_split_asm_thms, []),
  21.266 +           (split_selN, split_sel_thms, []),
  21.267 +           (split_sel_asmN, split_sel_asm_thms, []),
  21.268             (splitN, [split_thm], []),
  21.269             (split_asmN, [split_asm_thm], []),
  21.270 -           (splitsN, [split_thm, split_asm_thm], []),
  21.271 -           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
  21.272 +           (splitsN, [split_thm, split_asm_thm], [])]
  21.273            |> filter_out (null o #2)
  21.274            |> map (fn (thmN, thms, attrs) =>
  21.275              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
  21.276 @@ -1019,12 +1017,12 @@
  21.277          val ctr_sugar =
  21.278            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
  21.279             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
  21.280 -           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
  21.281 +           case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
  21.282             split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
  21.283             disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
  21.284 -           disc_excludesss = disc_exclude_thmsss, disc_exhausts = disc_exhaust_thms,
  21.285 -           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
  21.286 -           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
  21.287 +           distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
  21.288 +           exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
  21.289 +           split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
  21.290             case_eq_ifs = case_eq_if_thms}
  21.291            |> morph_ctr_sugar (substitute_noted_thm noted);
  21.292        in
    22.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
    22.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
    22.3 @@ -22,13 +22,13 @@
    22.4    val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
    22.5      thm list list -> tactic
    22.6    val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    22.7 -  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    22.8 +  val mk_exhaust_disc_tac: int -> thm -> thm list -> tactic
    22.9 +  val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic
   22.10    val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
   22.11      thm list list list -> thm list list list -> tactic
   22.12 -  val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
   22.13 +  val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic
   22.14    val mk_nchotomy_tac: int -> thm -> tactic
   22.15 -  val mk_other_half_disc_exclude_tac: thm -> tactic
   22.16 -  val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
   22.17 +  val mk_other_half_distinct_disc_tac: thm -> tactic
   22.18    val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list ->
   22.19      thm list list list -> tactic
   22.20    val mk_split_asm_tac: Proof.context -> thm -> tactic
   22.21 @@ -67,21 +67,21 @@
   22.22      (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
   22.23       |> k = 1 ? swap |> op @)));
   22.24  
   22.25 -fun mk_half_disc_exclude_tac ctxt m discD disc' =
   22.26 +fun mk_half_distinct_disc_tac ctxt m discD disc' =
   22.27    HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
   22.28      rtac disc');
   22.29  
   22.30 -fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
   22.31 +fun mk_other_half_distinct_disc_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
   22.32  
   22.33 -fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
   22.34 +fun mk_exhaust_disc_or_sel_tac n exhaust destIs =
   22.35    HEADGOAL (rtac exhaust THEN'
   22.36      EVERY' (map2 (fn k => fn destI => dtac destI THEN'
   22.37        select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
   22.38  
   22.39 -val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
   22.40 +val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac;
   22.41  
   22.42 -fun mk_sel_exhaust_tac n disc_exhaust collapses =
   22.43 -  mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
   22.44 +fun mk_exhaust_sel_tac n exhaust_disc collapses =
   22.45 +  mk_exhaust_disc_or_sel_tac n exhaust_disc collapses ORELSE
   22.46    HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
   22.47  
   22.48  fun mk_collapse_tac ctxt m discD sels =
   22.49 @@ -92,17 +92,17 @@
   22.50         REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
   22.51         SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
   22.52  
   22.53 -fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
   22.54 -    disc_excludesss' =
   22.55 +fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss
   22.56 +    distinct_discsss' =
   22.57    if ms = [0] then
   22.58      HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
   22.59 -      TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
   22.60 +      TRY o EVERY' [rtac uexhaust_disc, atac, rtac vexhaust_disc, atac])
   22.61    else
   22.62      let val ks = 1 upto n in
   22.63 -      HEADGOAL (rtac udisc_exhaust THEN'
   22.64 -        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
   22.65 -          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vdisc_exhaust,
   22.66 -            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
   22.67 +      HEADGOAL (rtac uexhaust_disc THEN'
   22.68 +        EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
   22.69 +          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
   22.70 +            EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
   22.71                EVERY'
   22.72                  (if k' = k then
   22.73                     [rtac (vuncollapse RS trans), TRY o atac] @
   22.74 @@ -113,11 +113,11 @@
   22.75                         REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
   22.76                         asm_simp_tac (ss_only [] ctxt)])
   22.77                   else
   22.78 -                   [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
   22.79 +                   [dtac (the_single (if k = n then distinct_discs else distinct_discs')),
   22.80                      etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
   22.81                      atac, atac]))
   22.82 -              ks disc_excludess disc_excludess' uncollapses)])
   22.83 -          ks ms disc_excludesss disc_excludesss' uncollapses))
   22.84 +              ks distinct_discss distinct_discss' uncollapses)])
   22.85 +          ks ms distinct_discsss distinct_discsss' uncollapses))
   22.86      end;
   22.87  
   22.88  fun mk_case_same_ctr_tac ctxt injects =
    23.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 15:03:25 2014 +0200
    23.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Aug 18 17:19:58 2014 +0200
    23.3 @@ -27,7 +27,7 @@
    23.4      case_name : string,
    23.5      case_rewrites : thm list,
    23.6      case_cong : thm,
    23.7 -    weak_case_cong : thm,
    23.8 +    case_cong_weak : thm,
    23.9      split : thm,
   23.10      split_asm: thm}
   23.11  end
   23.12 @@ -195,7 +195,7 @@
   23.13     case_name : string,
   23.14     case_rewrites : thm list,
   23.15     case_cong : thm,
   23.16 -   weak_case_cong : thm,
   23.17 +   case_cong_weak : thm,
   23.18     split : thm,
   23.19     split_asm: thm};
   23.20  
    24.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Aug 18 15:03:25 2014 +0200
    24.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Aug 18 17:19:58 2014 +0200
    24.3 @@ -95,7 +95,7 @@
    24.4    head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
    24.5  
    24.6  fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
    24.7 -    weak_case_cong, split, split_asm, ...} : Datatype_Aux.info) =
    24.8 +    case_cong_weak, split, split_asm, ...} : Datatype_Aux.info) =
    24.9    {ctrs = ctrs_of_exhaust exhaust,
   24.10     casex = case_of_case_rewrite (hd case_rewrites),
   24.11     discs = [],
   24.12 @@ -106,7 +106,7 @@
   24.13     distincts = distinct,
   24.14     case_thms = case_rewrites,
   24.15     case_cong = case_cong,
   24.16 -   weak_case_cong = weak_case_cong,
   24.17 +   case_cong_weak = case_cong_weak,
   24.18     split = split,
   24.19     split_asm = split_asm,
   24.20     disc_defs = [],
   24.21 @@ -114,13 +114,13 @@
   24.22     discIs = [],
   24.23     sel_defs = [],
   24.24     sel_thmss = [],
   24.25 -   disc_excludesss = [],
   24.26 -   disc_exhausts = [],
   24.27 -   sel_exhausts = [],
   24.28 +   distinct_discsss = [],
   24.29 +   exhaust_discs = [],
   24.30 +   exhaust_sels = [],
   24.31     collapses = [],
   24.32     expands = [],
   24.33 -   sel_splits = [],
   24.34 -   sel_split_asms = [],
   24.35 +   split_sels = [],
   24.36 +   split_sel_asms = [],
   24.37     case_eq_ifs = []};
   24.38  
   24.39  fun register dt_infos =
    25.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Aug 18 15:03:25 2014 +0200
    25.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Aug 18 17:19:58 2014 +0200
    25.3 @@ -18,7 +18,7 @@
    25.4    val make_cases : string list -> descr list -> theory -> term list list
    25.5    val make_splits : string list -> descr list -> theory -> (term * term) list
    25.6    val make_case_combs : string list -> descr list -> theory -> string -> term list
    25.7 -  val make_weak_case_congs : string list -> descr list -> theory -> term list
    25.8 +  val make_case_cong_weaks : string list -> descr list -> theory -> term list
    25.9    val make_case_congs : string list -> descr list -> theory -> term list
   25.10    val make_nchotomys : descr list -> term list
   25.11  end;
   25.12 @@ -330,7 +330,7 @@
   25.13  
   25.14  (************************* additional rules for TFL ***************************)
   25.15  
   25.16 -fun make_weak_case_congs case_names descr thy =
   25.17 +fun make_case_cong_weaks case_names descr thy =
   25.18    let
   25.19      val case_combs = make_case_combs case_names descr thy "f";
   25.20  
    26.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Aug 18 15:03:25 2014 +0200
    26.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Aug 18 17:19:58 2014 +0200
    26.3 @@ -395,16 +395,16 @@
    26.4      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
    26.5    end;
    26.6  
    26.7 -fun prove_weak_case_congs new_type_names case_names descr thy =
    26.8 +fun prove_case_cong_weaks new_type_names case_names descr thy =
    26.9    let
   26.10 -    fun prove_weak_case_cong t =
   26.11 +    fun prove_case_cong_weak t =
   26.12       Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   26.13         (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
   26.14  
   26.15 -    val weak_case_congs =
   26.16 -      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
   26.17 +    val case_cong_weaks =
   26.18 +      map prove_case_cong_weak (Datatype_Prop.make_case_cong_weaks case_names descr thy);
   26.19  
   26.20 -  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
   26.21 +  in thy |> Datatype_Aux.store_thms "case_cong_weak" new_type_names case_cong_weaks end;
   26.22  
   26.23  
   26.24  (* additional theorems for TFL *)
   26.25 @@ -470,7 +470,7 @@
   26.26  
   26.27  fun make_dt_info descr induct inducts rec_names rec_rewrites
   26.28      (index, (((((((((((_, (tname, _, _))), inject), distinct),
   26.29 -      exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
   26.30 +      exhaust), nchotomy), case_name), case_rewrites), case_cong), case_cong_weak),
   26.31          (split, split_asm))) =
   26.32    (tname,
   26.33     {index = index,
   26.34 @@ -486,7 +486,7 @@
   26.35      case_name = case_name,
   26.36      case_rewrites = case_rewrites,
   26.37      case_cong = case_cong,
   26.38 -    weak_case_cong = weak_case_cong,
   26.39 +    case_cong_weak = case_cong_weak,
   26.40      split = split,
   26.41      split_asm = split_asm});
   26.42  
   26.43 @@ -513,8 +513,8 @@
   26.44        |> prove_case_thms config new_type_names descr rec_names rec_rewrites;
   26.45      val (case_congs, thy7) = thy6
   26.46        |> prove_case_congs new_type_names case_names descr nchotomys case_rewrites;
   26.47 -    val (weak_case_congs, thy8) = thy7
   26.48 -      |> prove_weak_case_congs new_type_names case_names descr;
   26.49 +    val (case_cong_weaks, thy8) = thy7
   26.50 +      |> prove_case_cong_weaks new_type_names case_names descr;
   26.51      val (splits, thy9) = thy8
   26.52        |> prove_split_thms config new_type_names case_names descr
   26.53          inject distinct exhaust case_rewrites;
   26.54 @@ -524,7 +524,7 @@
   26.55        map_index
   26.56          (make_dt_info flat_descr induct inducts rec_names rec_rewrites)
   26.57          (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
   26.58 -          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
   26.59 +          case_names ~~ case_rewrites ~~ case_congs ~~ case_cong_weaks ~~ splits);
   26.60      val dt_names = map fst dt_infos;
   26.61      val prfx = Binding.qualify true (space_implode "_" new_type_names);
   26.62      val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
   26.63 @@ -553,7 +553,7 @@
   26.64          ((Binding.empty, [iff_add]), [(flat inject, [])]),
   26.65          ((Binding.empty, [Classical.safe_elim NONE]),
   26.66            [(map (fn th => th RS notE) (flat distinct), [])]),
   26.67 -        ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
   26.68 +        ((Binding.empty, [Simplifier.cong_add]), [(case_cong_weaks, [])]),
   26.69          ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
   26.70            named_rules @ unnamed_rules)
   26.71      |> snd
    27.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Aug 18 15:03:25 2014 +0200
    27.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Aug 18 17:19:58 2014 +0200
    27.3 @@ -190,7 +190,7 @@
    27.4  (* FIXME: put other record thms here, or declare as "no_atp" *)
    27.5  fun multi_base_blacklist ctxt ho_atp =
    27.6    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
    27.7 -   "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nat_of_char_simps", "nibble.simps",
    27.8 +   "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps",
    27.9     "nibble.distinct"]
   27.10    |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
   27.11    |> map (prefix Long_Name.separator)
    28.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon Aug 18 15:03:25 2014 +0200
    28.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon Aug 18 17:19:58 2014 +0200
    28.3 @@ -434,7 +434,7 @@
    28.4       val case_simpset =
    28.5         put_simpset HOL_basic_ss ctxt
    28.6            addsimps case_rewrites
    28.7 -          |> fold (Simplifier.add_cong o #weak_case_cong o snd)
    28.8 +          |> fold (Simplifier.add_cong o #case_cong_weak o snd)
    28.9                (Symtab.dest (Datatype.get_all theory))
   28.10       val corollaries' = map (Simplifier.simplify case_simpset) corollaries
   28.11       val extract = Rules.CONTEXT_REWRITE_RULE
    29.1 --- a/src/HOL/Tools/record.ML	Mon Aug 18 15:03:25 2014 +0200
    29.2 +++ b/src/HOL/Tools/record.ML	Mon Aug 18 17:19:58 2014 +0200
    29.3 @@ -1785,10 +1785,10 @@
    29.4    Ctr_Sugar.default_register_ctr_sugar_global T_name
    29.5      {ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
    29.6       nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
    29.7 -     case_cong = Drule.dummy_thm, weak_case_cong = Drule.dummy_thm, split = Drule.dummy_thm,
    29.8 +     case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
    29.9       split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
   29.10 -     sel_thmss = [sel_thms], disc_excludesss = [], disc_exhausts = [], sel_exhausts = [],
   29.11 -     collapses = [], expands = [], sel_splits = [], sel_split_asms = [], case_eq_ifs = []};
   29.12 +     sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
   29.13 +     collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
   29.14  
   29.15  
   29.16  (* definition *)