author | boehmes |
Wed, 08 Dec 2010 08:33:04 +0100 | |
changeset 41073 | 07b454783ed8 |
parent 41072 | 9f9bc1bdacef |
child 41074 | 286255f131bf |
--- a/src/HOL/Tools/SMT/smt_builtin.ML Wed Dec 08 08:33:02 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Wed Dec 08 08:33:04 2010 +0100 @@ -226,6 +226,8 @@ fun is_builtin_ext ctxt (c as (n, _)) ts = if member (op =) only_partially_supported n then false - else is_builtin_fun_ext ctxt c ts + else + is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse + is_builtin_fun_ext ctxt c ts end