
diff -r b1e1508643b1 -r 16b4f5774621 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Nov 20 21:07:10 2011 +0100
@@ -14,8 +14,8 @@
   ("Tools/nat_numeral_simprocs.ML")
 begin
 
-declare split_div [of _ _ "number_of k", standard, arith_split]
-declare split_mod [of _ _ "number_of k", standard, arith_split]
+declare split_div [of _ _ "number_of k", arith_split] for k
+declare split_mod [of _ _ "number_of k", arith_split] for k
 
 text {* For @{text combine_numerals} *}
 




