src/HOL/Tools/SMT/smt_translate.ML
changeset 41057 8dbc951a291c
parent 40697 c3979dd80a50
child 41059 d2b1fc1b8e19
     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