simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
authorhaftmann
Sun Nov 10 10:02:34 2013 +0100 (2013-11-10)
changeset 54293cd896760fa0f
parent 54292 ce4a17b2e373
child 54294 98826791a588
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
src/HOL/Tools/SMT/smt_normalize.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Nov 08 21:40:07 2013 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Nov 10 10:02:34 2013 +0100
     1.3 @@ -532,9 +532,7 @@
     1.4    *)
     1.5  
     1.6    fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
     1.7 -        (case try HOLogic.dest_number t of
     1.8 -          SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
     1.9 -        | NONE => false)
    1.10 +        SMT_Builtin.is_builtin_num ctxt t
    1.11      | is_strange_number _ _ = false
    1.12  
    1.13    val pos_num_ss =