--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 06 15:38:02 2010 +0100
@@ -194,7 +194,7 @@
| is_builtin_conn' (@{const_name False}, _) = false
| is_builtin_conn' c = is_builtin_conn c
- fun is_builtin_pred' ctxt (@{const_name distinct}, _) [t] =
+ fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
is_builtin_distinct andalso can HOLogic.dest_list t
| is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 06 15:38:02 2010 +0100
@@ -195,7 +195,7 @@
fun builtin_fun ctxt (c as (n, T)) ts =
let
val builtin_func' = chained_builtin_func (get_builtins ctxt)
- fun builtin_pred' c t =
+ fun builtin_pred' c ts =
(case distinct_pred c ts of
SOME b => SOME b
| NONE => chained_builtin_pred (get_builtins ctxt) c ts)