src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -45,8 +45,7 @@
   nat = Nat
   by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
 
-constdefs
-  Suc ::   "nat => nat"
+definition Suc :: "nat => nat" where
   Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
 
 local