swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)

--- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 13:31:12 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 15:33:35 2010 +0100
@@ -9,8 +9,8 @@
 
 signature SMT_BUILTIN =
 sig
+  val is_builtin: Proof.context -> string * typ -> bool
   val is_partially_builtin: Proof.context -> string * typ -> bool
-  val is_builtin: Proof.context -> string * typ -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
@@ -109,8 +109,8 @@
     SOME proper_type => proper_type T
   | NONE => false)
 
-fun is_partially_builtin _ = lookup_builtin builtins
+fun is_builtin _ = lookup_builtin builtins
 
-fun is_builtin _ = lookup_builtin all_builtins
+fun is_partially_builtin _ = lookup_builtin all_builtins
 
 end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 13:31:12 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 15:33:35 2010 +0100
@@ -263,7 +263,7 @@
     | _ =>
         (case Term.strip_comb (Thm.term_of ct) of
           (Const (c as (_, T)), ts) =>
-            if SMT_Builtin.is_builtin ctxt c
+            if SMT_Builtin.is_partially_builtin ctxt c
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv