# HG changeset patch
# User boehmes
# Date 1289573766 -3600
# Node ID fd218201da5e29328783f33f8483f0b076d5c42a
# Parent  094e5d1f5bafb3d16cddcceb8c8fda44805c197e
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

diff -r 094e5d1f5baf -r fd218201da5e src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Nov 12 06:11:29 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Nov 12 15:56:06 2010 +0100
@@ -17,8 +17,7 @@
 
 val ignored = member (op =) [
   @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
-  @{const_name HOL.eq}, @{const_name zero_class.zero},
-  @{const_name one_class.one}, @{const_name number_of}]
+  @{const_name HOL.eq}]
 
 fun is_const f (n, T) = not (ignored n) andalso f T
 fun add_const_if f g (Const c) = if is_const f c then g c else I