src/HOL/Tools/numeral_simprocs.ML

--- a/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 00:08:39 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Mar 27 02:10:00 2010 +0100
@@ -344,8 +344,7 @@
 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;
+  val is_numeral = can HOLogic.dest_number
 end;
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);