diff -r 83f241623b86 -r 8dbc951a291c src/HOL/Tools/SMT/smt_translate.ML
--- 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