src/HOL/Tools/int_arith.ML

--- a/src/HOL/Tools/int_arith.ML	Thu Mar 26 14:30:20 2009 +0000
+++ b/src/HOL/Tools/int_arith.ML	Thu Mar 26 11:33:50 2009 -0700
@@ -377,6 +377,8 @@
 struct
   val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   val eq_reflection = eq_reflection
+  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
+    | is_numeral _ = false;
 end;
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);