--- a/src/HOL/Real/RealDef.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Tue Jul 31 00:56:26 2007 +0200
@@ -832,8 +832,7 @@
use "real_arith.ML"
-
-setup real_arith_setup
+declaration {* K real_arith_setup *}
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}