changeset 41057 | 8dbc951a291c |
parent 40697 | c3979dd80a50 |
child 41059 | d2b1fc1b8e19 |
--- 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