src/HOL/Tools/SMT/smt_normalize.ML
changeset 54293 cd896760fa0f
parent 54041 227908156cd2
child 54489 03ff4d1e6784
     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 =