--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 14:20:34 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 14:32:24 2010 +0200
@@ -205,7 +205,6 @@
val is_choice_spec_fun : hol_context -> styp -> bool
val is_choice_spec_axiom : theory -> const_table -> term -> bool
val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool
- val is_equational_fun : hol_context -> styp -> bool
val codatatype_bisim_axioms : hol_context -> typ -> term list
val is_well_founded_inductive_pred : hol_context -> styp -> bool
val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
@@ -1493,10 +1492,6 @@
fun is_equational_fun_but_no_plain_def hol_ctxt =
(is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
(String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
-fun is_equational_fun (hol_ctxt as {ctxt, thy, def_table, ...}) (x as (s, _)) =
- is_equational_fun_but_no_plain_def hol_ctxt x orelse
- (not (is_choice_spec_fun hol_ctxt x) andalso
- is_some (def_of_const thy def_table x))
(** Constant unfolding **)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 14:20:34 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 14:32:24 2010 +0200
@@ -730,8 +730,9 @@
x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso
forall (op aconv) (ts1 ~~ ts2)
-fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
- special_funs, ...}) depth t =
+fun specialize_consts_in_term
+ (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table,
+ simp_table, special_funs, ...}) depth t =
if not specialize orelse depth > special_max_depth then
t
else
@@ -741,7 +742,12 @@
fun aux args Ts (Const (x as (s, T))) =
((if not (member (op =) blacklist x) andalso not (null args) andalso
not (String.isPrefix special_prefix s) andalso
- is_equational_fun hol_ctxt x then
+ not (is_built_in_const thy stds fast_descrs x) andalso
+ (is_equational_fun_but_no_plain_def hol_ctxt x orelse
+ (is_some (def_of_const thy def_table x) andalso
+ not (is_of_class_const thy x) andalso
+ not (is_constr ctxt stds x) andalso
+ not (is_choice_spec_fun hol_ctxt x))) then
let
val eligible_args = filter (is_eligible_arg Ts o snd)
(index_seq 0 (length args) ~~ args)