# HG changeset patch # User boehmes # Date 1290609215 -3600 # Node ID 4725ed462387d898a47494053f0f0136962697f4 # Parent dcb27631cb45be854fb76197a41481567ec96172 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) diff -r dcb27631cb45 -r 4725ed462387 src/HOL/Tools/SMT/smt_builtin.ML --- 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 diff -r dcb27631cb45 -r 4725ed462387 src/HOL/Tools/SMT/smt_normalize.ML --- 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