src/HOL/RealDef.thy

--- a/src/HOL/RealDef.thy	Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/RealDef.thy	Mon Jul 12 08:58:13 2010 +0200
@@ -751,7 +751,7 @@
 begin
 
 definition
-  "(number_of x :: real) = of_int x"
+  [code del]: "(number_of x :: real) = of_int x"
 
 instance proof
 qed (rule number_of_real_def)
@@ -1498,8 +1498,6 @@
 
 subsection{*Numerals and Arithmetic*}
 
-declare number_of_real_def [code del]
-
 lemma [code_unfold_post]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id number_of_real_def ..