# HG changeset patch
# User haftmann
# Date 1384074154 -3600
# Node ID cd896760fa0f1fde412fd16130ee7ed09af50c99
# Parent  ce4a17b2e3739aa9a0a5e387f431e302f83028ec
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number

diff -r ce4a17b2e373 -r cd896760fa0f src/HOL/Tools/SMT/smt_normalize.ML
--- 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 =