src/HOL/Library/Float.thy

--- a/src/HOL/Library/Float.thy	Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Float.thy	Tue Jul 14 16:27:32 2009 +0200
@@ -42,7 +42,7 @@
 instance ..
 end
 
-lemma number_of_float_Float [code_inline, symmetric, code_post]:
+lemma number_of_float_Float [code_unfold_post]:
   "number_of k = Float (number_of k) 0"
   by (simp add: number_of_float_def number_of_is_id)