# HG changeset patch
# User blanchet
# Date 1392937796 -3600
# Node ID 63beb38e9258bbd3649d811e6b59de11c56770d5
# Parent  5b466efedd2c76f01fdc1ae60cfa8eb4b2f041a6
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -81,7 +81,7 @@
 
 lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
 unfolding fstOp_def mem_Collect_eq
-by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
+by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
 
 lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
 unfolding comp_def fstOp_def by simp
@@ -91,7 +91,7 @@
 
 lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
 unfolding sndOp_def mem_Collect_eq
-by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
+by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
 
 lemma csquare_fstOp_sndOp:
 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -20,7 +20,7 @@
 by blast
 
 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
-by (cases u) (hypsubst, rule unit.cases)
+by (cases u) (hypsubst, rule unit.case)
 
 lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
 by simp
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -107,7 +107,7 @@
 
 subsubsection {* Code generator setup *}
 
-lemmas [code del] = term.recs term.cases term.size
+lemmas [code del] = term.rec term.case term.size
 lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
 
 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -888,7 +888,7 @@
   "case_natural f g n = (if n = 0 then f else g (n - 1))"
   by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
 
-declare natural.recs [code del]
+declare natural.rec [code del]
 
 lemma [code abstract]:
   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Datatype.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -133,7 +133,7 @@
 
 lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
 apply (simp add: Node_def Push_def) 
-apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
+apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
 done
 
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Extraction.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -280,28 +280,28 @@
   conjunct2: "Null" "conjunct2"
 
   disjI1 (P, Q): "Inl"
-    "\<^bold>\<lambda>(c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
+    "\<^bold>\<lambda>(c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
 
   disjI1 (P): "Some"
-    "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
+    "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
 
   disjI1 (Q): "None"
-    "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
+    "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
 
   disjI1: "Left"
-    "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
+    "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
 
   disjI2 (P, Q): "Inr"
-    "\<^bold>\<lambda>(d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
+    "\<^bold>\<lambda>(d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
 
   disjI2 (P): "None"
-    "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
+    "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
 
   disjI2 (Q): "Some"
-    "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
+    "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
 
   disjI2: "Right"
-    "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
+    "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
 
   disjE (P, Q, R): "\<lambda>pq pr qr.
      (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -74,7 +74,7 @@
 subsection {* Continuity of @{const case_lift} *}
 
 lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
-apply (induct x, unfold lift.cases)
+apply (induct x, unfold lift.case)
 apply (simp add: Rep_lift_strict)
 apply (simp add: Def_def Abs_lift_inverse)
 done
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -52,8 +52,8 @@
 code_datatype Lazy_Sequence
 
 declare list_of_lazy_sequence.simps [code del]
-declare lazy_sequence.cases [code del]
-declare lazy_sequence.recs [code del]
+declare lazy_sequence.case [code del]
+declare lazy_sequence.rec [code del]
 
 lemma list_of_Lazy_Sequence [simp]:
   "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -406,7 +406,7 @@
   { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
     assume "\<forall>m\<in>set ms. m > 0"
     then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
-      by (induct ms) (auto, metis Suc_pred' nat.cases(2)) }
+      by (induct ms) (auto, metis Suc_pred' nat.case(2)) }
   note * = this
   show ?thesis
     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
@@ -452,7 +452,7 @@
 lemma coeff_Poly_eq:
   "coeff (Poly xs) n = nth_default 0 xs n"
   apply (induct xs arbitrary: n) apply simp_all
-  by (metis nat.cases not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
+  by (metis nat.case not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
 
 lemma nth_default_coeffs_eq:
   "nth_default 0 (coeffs p) = coeff p"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -1753,8 +1753,8 @@
 hide_fact (open)
   Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
   Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
-  compare.simps compare.exhaust compare.induct compare.recs compare.simps
-  compare.size compare.case_cong compare.weak_case_cong compare.cases 
+  compare.simps compare.exhaust compare.induct compare.rec compare.simps
+  compare.size compare.case_cong compare.weak_case_cong compare.case
   compare.nchotomy compare.split compare.split_asm rec_compare_def
   compare.eq.refl compare.eq.simps
   compare.EQ_def compare.GT_def compare.LT_def
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -1645,10 +1645,10 @@
 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
 apply (induct xs, simp, simp)
 apply safe
-apply (metis nat.cases(1) nth.simps zero_less_Suc)
+apply (metis nat.case(1) nth.simps zero_less_Suc)
 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
 apply (case_tac i, simp)
-apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc nat.case(2) nth.simps zero_less_diff)
 done
 
 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -112,9 +112,8 @@
 
 lemmas induct = old.nat.induct
 lemmas inducts = old.nat.inducts
-lemmas recs = old.nat.recs
-lemmas cases = nat.case
-lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
+lemmas rec = old.nat.rec
+lemmas simps = nat.inject nat.distinct nat.case nat.rec
 
 setup {* Sign.parent_path *}
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Nitpick.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -101,17 +101,17 @@
 lemma case_unit_unfold [nitpick_unfold]:
 "case_unit x u \<equiv> x"
 apply (subgoal_tac "u = ()")
- apply (simp only: unit.cases)
+ apply (simp only: unit.case)
 by simp
 
-declare unit.cases [nitpick_simp del]
+declare unit.case [nitpick_simp del]
 
 lemma case_nat_unfold [nitpick_unfold]:
 "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
 apply (rule eq_reflection)
 by (cases n) auto
 
-declare nat.cases [nitpick_simp del]
+declare nat.case [nitpick_simp del]
 
 lemma list_size_simp [nitpick_simp]:
 "list_size f xs = (if xs = [] then 0
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -528,7 +528,7 @@
       with sbBB [of i] obtain j where "x \<in> BB i j"
         by blast
       thus "\<exists>i. x \<in> split BB (prod_decode i)"
-        by (metis prod_encode_inverse prod.cases)
+        by (metis prod_encode_inverse prod.case)
     qed
     have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
       by (rule ext)  (auto simp add: C_def)
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -196,7 +196,7 @@
           (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
         proof (induct k)
           case 0 with w0 show ?case
-            unfolding w_def nat.recs(1) by auto
+            unfolding w_def nat.rec(1) by auto
         next
           case (Suc k)
           then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
@@ -241,7 +241,7 @@
                  (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
           qed
           then have "?P k (w k) (w (Suc k))"
-            unfolding w_def nat.recs(2) unfolding w_def[symmetric]
+            unfolding w_def nat.rec(2) unfolding w_def[symmetric]
             by (rule someI_ex)
           then show ?case by auto
         qed
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -250,7 +250,7 @@
   { fix i have "A i \<in> sets M" unfolding A_def
     proof (induct i)
       case (Suc i)
-      from Ex_P[OF this, of i] show ?case unfolding nat.recs(2)
+      from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
         by (rule someI2_ex) simp
     qed simp }
   note A_in_sets = this
@@ -281,7 +281,7 @@
       from ex_inverse_of_nat_Suc_less[OF this]
       obtain n where *: "?d B < - 1 / real (Suc n)"
         by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
-      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
+      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
       from epsilon[OF B(1) this] *
       show False by auto
     qed
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Product_Type.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -29,9 +29,8 @@
 
 lemmas induct = old.bool.induct
 lemmas inducts = old.bool.inducts
-lemmas recs = old.bool.recs
-lemmas cases = bool.case
-lemmas simps = bool.distinct bool.case old.bool.recs
+lemmas rec = old.bool.rec
+lemmas simps = bool.distinct bool.case bool.rec
 
 setup {* Sign.parent_path *}
 
@@ -99,9 +98,8 @@
 
 lemmas induct = old.unit.induct
 lemmas inducts = old.unit.inducts
-lemmas recs = old.unit.recs
-lemmas cases = unit.case
-lemmas simps = unit.case old.unit.recs
+lemmas rec = old.unit.rec
+lemmas simps = unit.case unit.rec
 
 setup {* Sign.parent_path *}
 
@@ -217,9 +215,8 @@
 
 lemmas induct = old.prod.induct
 lemmas inducts = old.prod.inducts
-lemmas recs = old.prod.recs
-lemmas cases = prod.case
-lemmas simps = prod.inject prod.case old.prod.recs
+lemmas rec = old.prod.rec
+lemmas simps = prod.inject prod.case prod.rec
 
 setup {* Sign.parent_path *}
 
@@ -403,7 +400,7 @@
   by (simp add: prod_eq_iff)
 
 lemma split_conv [simp, code]: "split f (a, b) = f a b"
-  by (fact prod.cases)
+  by (fact prod.case)
 
 lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   by (rule split_conv [THEN iffD2])
@@ -684,7 +681,7 @@
   Setup of internal @{text split_rule}.
 *}
 
-lemmas case_prodI = prod.cases [THEN iffD2]
+lemmas case_prodI = prod.case [THEN iffD2]
 
 lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   by (fact splitI2)
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/String.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -289,7 +289,7 @@
 lemma case_char_code [code]:
   "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   by (cases c)
-    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
+    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
 
 lemma [code]:
   "rec_char = case_char"
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -114,9 +114,8 @@
 
 lemmas induct = old.sum.induct
 lemmas inducts = old.sum.inducts
-lemmas recs = old.sum.recs
-lemmas cases = sum.case
-lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
+lemmas rec = old.sum.rec
+lemmas simps = sum.inject sum.distinct sum.case sum.rec
 
 setup {* Sign.parent_path *}
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -257,7 +257,7 @@
            ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
              map_comp RS sym, map_id]) RSN (2, trans))),
         REPEAT_DETERM_N (2 * live) o atac,
-        REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
+        REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
         rtac refl,
         rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}),
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -35,7 +35,7 @@
 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
 
-val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps};
+val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
 val sum_prod_thms_set0 =
   @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
       Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -468,8 +468,8 @@
 
 fun mk_sum_caseN_balanced 1 1 = refl
   | mk_sum_caseN_balanced n k =
-    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm case_sum_step(1)},
-      right = mk_sum_step @{thm sum.cases(2)} @{thm case_sum_step(2)}, init = refl} n k;
+    Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
+      right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
 
 fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   let
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -1129,7 +1129,7 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val strT_defs = map (fn def =>
-        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
+        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.case}])
       strT_def_frees;
     val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -138,7 +138,7 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
-       sum.cases} @ mapsx @ map_comps @ map_idents))) ORELSE'
+       sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
     fo_rtac @{thm cong} ctxt ORELSE'
     rtac ext));
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -751,7 +751,7 @@
 
 fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
   unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
-    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
+    rtac trans, rtac unfold, fo_rtac (@{thm sum.case(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
@@ -1033,8 +1033,8 @@
           rtac (map_comp0 RS trans), rtac (map_cong RS trans),
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]},
           REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
-          etac (@{thm prod.cases} RS map_arg_cong RS trans),
-          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
+          etac (@{thm prod.case} RS map_arg_cong RS trans),
+          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case}), 
           CONJ_WRAP' (fn set_map0 =>
             EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
               dtac (set_map0 RS equalityD1 RS set_mp),
@@ -1046,7 +1046,7 @@
       ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1
   end;
 
-val split_id_unfolds = @{thms prod.cases image_id id_apply};
+val split_id_unfolds = @{thms prod.case image_id id_apply};
 
 fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   let val n = length ks;
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -44,7 +44,7 @@
 fun meta thm = thm RS eq_reflection
 
 fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
-  (map meta (@{thm split_conv} :: @{thms sum.cases}))
+  (map meta (@{thm split_conv} :: @{thms sum.case}))
 
 fun term_conv thy cv t =
   cv (cterm_of thy t)
@@ -315,7 +315,7 @@
         val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
           |> Goal.init
           |> (Simplifier.rewrite_goals_tac ctxt
-                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
               THEN CONVERSION (ind_rulify ctxt) 1)
           |> Seq.hd
           |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -129,7 +129,7 @@
   THEN rtac @{thm CollectI} 1
   THEN etac @{thm conjE} 1
   THEN etac @{thm ssubst} 1
-  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
+  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
 
 (* Sets *)
 
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/Function/sum_tree.ML
--- a/src/HOL/Tools/Function/sum_tree.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -22,7 +22,7 @@
 (* Theory dependencies *)
 val sumcase_split_ss =
   simpset_of (put_simpset HOL_basic_ss @{context}
-    addsimps (@{thm Product_Type.split} :: @{thms sum.cases}))
+    addsimps (@{thm Product_Type.split} :: @{thms sum.case}))
 
 (* top-down access in balanced tree *)
 fun access_top_down {left, right, init} len i =
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -145,7 +145,7 @@
           fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
         end
       else []
-    val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
+    val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"}
       (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   in
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -774,7 +774,7 @@
   |> map nickname_of_thm
 
 fun is_size_def [dep] th =
-    (case first_field ".recs" dep of
+    (case first_field ".rec" dep of
        SOME (pref, _) =>
        (case first_field ".size" (nickname_of_thm th) of
           SOME (pref', _) => pref = pref'
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -323,14 +323,14 @@
     THEN' (REPEAT_DETERM1 o
       (rtac @{thm refl}
       ORELSE' rtac
-        @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
+        @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
       ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
         (HOLogic.Trueprop_conv
           (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
 
 fun elim_image_tac ctxt = etac @{thm imageE}
   THEN' REPEAT_DETERM o CHANGED o
-    (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
+    (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
     THEN' REPEAT_DETERM o etac @{thm Pair_inject}
     THEN' TRY o hyp_subst_tac ctxt)
 
@@ -348,13 +348,13 @@
     REPEAT_DETERM1 o (atac
       ORELSE' rtac @{thm SigmaI}
       ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
-        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
+        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
       ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
-        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
+        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
       ORELSE' (rtac @{thm image_eqI} THEN'
     (REPEAT_DETERM o
       (rtac @{thm refl}
-      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]})))
+      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
       ORELSE' rtac @{thm UNIV_I}
       ORELSE' rtac @{thm iffD2[OF Compl_iff]}
       ORELSE' atac)
@@ -375,16 +375,16 @@
        ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
        ORELSE' etac @{thm conjE}
        ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
-         TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
+         TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
          REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
        ORELSE' (etac @{thm imageE}
          THEN' (REPEAT_DETERM o CHANGED o
-         (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
+         (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
          THEN' REPEAT_DETERM o etac @{thm Pair_inject}
          THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
        ORELSE' etac @{thm ComplE}
        ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
-        THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
+        THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
         THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
 
 fun tac ctxt fm =
@@ -427,7 +427,7 @@
         HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
       end;
     fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
-    val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases}
+    val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
     fun tac ctxt = 
       rtac @{thm set_eqI}
       THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -1298,7 +1298,7 @@
   assume *: "\<forall>n. \<exists>p. ?P p n"
   def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
   have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
   have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
   have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
   then have "subseq f" unfolding subseq_Suc_iff by auto
@@ -1320,7 +1320,7 @@
   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
   def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
   have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
   have P_0: "?P (f 0) (Suc N)"
     unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
   { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"