# HG changeset patch
# User blanchet
# Date 1290641550 -3600
# Node ID a68f64f998328724cd183cd7e917b024b7329aba
# Parent  3f472e57446a05cf7a788a261c62aca0dbc66266
fix check for builtinness of 0 and 1 -- these aren't functions

diff -r 3f472e57446a -r a68f64f99832 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Thu Nov 25 00:17:16 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Thu Nov 25 00:32:30 2010 +0100
@@ -69,8 +69,8 @@
   (@{const_name HOL.eq}, K true),
 
   (* numerals *)
-  (@{const_name zero_class.zero}, is_arithT_dom),
-  (@{const_name one_class.one}, is_arithT_dom),
+  (@{const_name zero_class.zero}, is_arithT),
+  (@{const_name one_class.one}, is_arithT),
   (@{const_name Int.Pls}, K true),
   (@{const_name Int.Min}, K true),
   (@{const_name Int.Bit0}, K true),