src/HOL/Tools/SMT/smt_normalize.ML
changeset 40686 4725ed462387
parent 40685 dcb27631cb45
child 41059 d2b1fc1b8e19
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 13:31:12 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 15:33:35 2010 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4      | _ =>
     1.5          (case Term.strip_comb (Thm.term_of ct) of
     1.6            (Const (c as (_, T)), ts) =>
     1.7 -            if SMT_Builtin.is_builtin ctxt c
     1.8 +            if SMT_Builtin.is_partially_builtin ctxt c
     1.9              then eta_args_conv norm_conv
    1.10                (length (Term.binder_types T) - length ts)
    1.11              else args_conv o norm_conv