simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Nov 08 21:40:07 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Nov 10 10:02:34 2013 +0100
@@ -532,9 +532,7 @@
   *)
 
   fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
-        (case try HOLogic.dest_number t of
-          SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
-        | NONE => false)
+        SMT_Builtin.is_builtin_num ctxt t
     | is_strange_number _ _ = false
 
   val pos_num_ss =