1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 06 13:46:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 06 15:38:02 2010 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4        | is_builtin_conn' (@{const_name False}, _) = false
     1.5        | is_builtin_conn' c = is_builtin_conn c
     1.6  
     1.7 -    fun is_builtin_pred' ctxt (@{const_name distinct}, _) [t] =
     1.8 +    fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
     1.9            is_builtin_distinct andalso can HOLogic.dest_list t
    1.10        | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
    1.11  

     2.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 06 13:46:45 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 06 15:38:02 2010 +0100
     2.3 @@ -195,7 +195,7 @@
     2.4  fun builtin_fun ctxt (c as (n, T)) ts =
     2.5    let
     2.6      val builtin_func' = chained_builtin_func (get_builtins ctxt)
     2.7 -    fun builtin_pred' c t =
     2.8 +    fun builtin_pred' c ts =
     2.9        (case distinct_pred c ts of
    2.10          SOME b => SOME b
    2.11        | NONE => chained_builtin_pred (get_builtins ctxt) c ts)