dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Nov 12 06:11:29 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Nov 12 15:56:06 2010 +0100
@@ -17,8 +17,7 @@
 
 val ignored = member (op =) [
   @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
-  @{const_name HOL.eq}, @{const_name zero_class.zero},
-  @{const_name one_class.one}, @{const_name number_of}]
+  @{const_name HOL.eq}]
 
 fun is_const f (n, T) = not (ignored n) andalso f T
 fun add_const_if f g (Const c) = if is_const f c then g c else I