# HG changeset patch
# User blanchet
# Date 1281011544 -7200
# Node ID 38339c0558697945adf4ada74e1321b4b5a36afa
# Parent  39e84a503840a469bfda6c46c900d85960e442db
don't specialize built-ins or constructors

diff -r 39e84a503840 -r 38339c055869 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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 **)
 
diff -r 39e84a503840 -r 38339c055869 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- 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)