1.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 13:31:12 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 15:33:35 2010 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  signature SMT_BUILTIN =
     1.6  sig
     1.7 +  val is_builtin: Proof.context -> string * typ -> bool
     1.8    val is_partially_builtin: Proof.context -> string * typ -> bool
     1.9 -  val is_builtin: Proof.context -> string * typ -> bool
    1.10  end
    1.11  
    1.12  structure SMT_Builtin: SMT_BUILTIN =
    1.13 @@ -109,8 +109,8 @@
    1.14      SOME proper_type => proper_type T
    1.15    | NONE => false)
    1.16  
    1.17 -fun is_partially_builtin _ = lookup_builtin builtins
    1.18 +fun is_builtin _ = lookup_builtin builtins
    1.19  
    1.20 -fun is_builtin _ = lookup_builtin all_builtins
    1.21 +fun is_partially_builtin _ = lookup_builtin all_builtins
    1.22  
    1.23  end

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