diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -783,7 +783,7 @@
   by (rule is_measure_trivial)
 
 
-subsection {* Inductive represenation of target language naturals *}
+subsection {* Inductive representation of target language naturals *}
 
 lift_definition Suc :: "natural \<Rightarrow> natural"
   is Nat.Suc
@@ -794,7 +794,7 @@
 rep_datatype "0::natural" Suc
   by (transfer, fact nat.induct nat.inject nat.distinct)+
 
-lemma natural_case [case_names nat, cases type: natural]:
+lemma natural_cases [case_names nat, cases type: natural]:
   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
@@ -876,7 +876,7 @@
   by transfer (simp add: fun_eq_iff)
 
 lemma [code, code_unfold]:
-  "natural_case f g n = (if n = 0 then f else g (n - 1))"
+  "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]