src/HOL/Int.thy

--- a/src/HOL/Int.thy	Fri Nov 07 08:57:15 2008 +0100
+++ b/src/HOL/Int.thy	Mon Nov 10 08:18:56 2008 +0100
@@ -782,11 +782,11 @@
 instantiation int :: number_ring
 begin
 
-definition
-  int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
+definition int_number_of_def [code del]:
+  "number_of w = (of_int w \<Colon> int)"
 
-instance
-  by intro_classes (simp only: int_number_of_def)
+instance proof
+qed (simp only: int_number_of_def)
 
 end