slightly more general simproc (avoids errors of linarith)

--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Mar 27 00:08:39 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sat Mar 27 02:10:00 2010 +0100
@@ -1143,6 +1143,7 @@
   addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
   addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
   addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
+  addsimps [@{thm mult_1_left}]
   addsimprocs [
     Simplifier.simproc @{theory} "fast_int_arith" [
       "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),

--- 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);