author | blanchet |
Thu, 25 Nov 2010 00:32:30 +0100 | |
changeset 40691 | a68f64f99832 |
parent 40690 | 3f472e57446a |
child 40692 | 7fa054c3f810 |
child 40705 | 03f1266a066e |
--- 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),