diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/NatBin.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -14,8 +14,15 @@
   Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
-instance nat :: number
-  nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
+instantiation nat :: number
+begin
+
+definition
+  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
+
+instance ..
+
+end
 
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where