diff -r c212b002fc8c -r a9671d4f7c03 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Nov 18 00:20:17 2006 +0100
+++ b/src/HOL/Nat.thy	Sat Nov 18 00:20:18 2006 +0100
@@ -111,16 +111,20 @@
 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   by auto
 
+text {* size of a datatype value *}
 
-text {* size of a datatype value; overloaded *}
-consts size :: "'a => nat"
+class size =
+  fixes size :: "'a \<Rightarrow> nat"
 
 text {* @{typ nat} is a datatype *}
 
 rep_datatype nat
   distinct  Suc_not_Zero Zero_not_Suc
   inject    Suc_Suc_eq
-  induction nat_induct [case_names 0 Suc]
+  induction nat_induct
+
+declare nat.induct [case_names 0 Suc, induct type: nat]
+declare nat.exhaust [case_names 0 Suc, cases type: nat]
 
 lemma n_not_Suc_n: "n \<noteq> Suc n"
   by (induct n) simp_all
@@ -472,11 +476,8 @@
 
 subsection {* Arithmetic operators *}
 
-axclass power < type
-
-consts
-  power :: "('a::power) => nat => 'a"            (infixr "^" 80)
-
+class power =
+  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}