--- a/src/HOL/RealDef.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Jul 12 10:48:37 2010 +0200
@@ -751,7 +751,7 @@
begin
definition
- [code del]: "(number_of x :: real) = of_int x"
+ "(number_of x :: real) = of_int x"
instance proof
qed (rule number_of_real_def)