# HG changeset patch
# User boehmes
# Date 1291793584 -3600
# Node ID 07b454783ed8074884ba1e9164d1f84ec1dd0536
# Parent  9f9bc1bdacef505398a946c6b4ff2b3ae99227d8
built-in numbers are also built-in terms

diff -r 9f9bc1bdacef -r 07b454783ed8 src/HOL/Tools/SMT/smt_builtin.ML
--- 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