
diff -r 40f414b87655 -r 366d4d234814 src/HOL/IntArith.thy
--- a/src/HOL/IntArith.thy	Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/IntArith.thy	Tue Jul 31 00:56:26 2007 +0200
@@ -115,7 +115,7 @@
  min_def[of "number_of u" "1::int", standard, simp]
 
 use "int_arith1.ML"
-setup int_arith_setup
+declaration {* K int_arith_setup *}
 
 
 subsection{*Lemmas About Small Numerals*}




