--- a/src/HOL/Nat.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Nat.thy Tue Jul 31 00:56:26 2007 +0200
@@ -1092,7 +1092,7 @@
using 2 1 by (rule trans)
use "arith_data.ML"
-setup arith_setup
+declaration {* K arith_setup *}
text{*The following proofs may rely on the arithmetic proof procedures.*}