| changeset 33017 | 4fb8a33f74d6 |
| parent 32618 | 42865636d006 |
| child 35153 | 5e8935678ee4 |
--- a/src/HOL/SMT/Tools/z3_interface.ML Tue Oct 20 12:06:17 2009 +0200 +++ b/src/HOL/SMT/Tools/z3_interface.ML Tue Oct 20 14:22:02 2009 +0200 @@ -88,7 +88,7 @@ (@{term word_sless}, "bvslt"), (@{term word_sle}, "bvsle")] -val builtins = T.Builtins { +val builtins = { builtin_typ = builtin_typ, builtin_num = builtin_num, builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }