# HG changeset patch
# User blanchet
# Date 1300200582 -3600
# Node ID 09b75d55008fcadaca779b002c61412636d756b4
# Parent  e5dba3d75e9e554e98a7238ce23720879b0e311b
support non-ground "need" values

diff -r e5dba3d75e9e -r 09b75d55008f doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Mar 15 13:03:54 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Mar 15 15:49:42 2011 +0100
@@ -2466,12 +2466,12 @@
 {\small See also \textit{debug} (\S\ref{output-format}).}
 
 \opnodefault{need}{term\_list}
-Specifies a list of datatype values (ground constructor terms) that should be
-part of the subterm-closed subsets used to approximate datatypes. If you know
-that a value must necessarily belong to the subset of representable values that
-approximates a datatype, specifying it can speed up the search, especially for
-high cardinalities. By default, Nitpick inspects the conjecture to infer needed
-datatype values.
+Specifies a list of datatype values (normally ground constructor terms) that
+should be part of the subterm-closed subsets used to approximate datatypes. If
+you know that a value must necessarily belong to the subset of representable
+values that approximates a datatype, specifying it can speed up the search,
+especially for high cardinalities.
+%By default, Nitpick inspects the conjecture to infer needed datatype values.
 
 \opsmart{total\_consts}{partial\_consts}
 Specifies whether constants occurring in the problem other than constructors can
diff -r e5dba3d75e9e -r 09b75d55008f src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 13:03:54 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 15:49:42 2011 +0100
@@ -197,10 +197,6 @@
 
 fun plazy f = Pretty.blk (0, pstrs (f ()))
 
-fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
-  | check_constr_nut _ =
-    error "The \"need\" option requires a constructor term."
-
 fun pick_them_nits_in_term deadline state (params : params) auto i n step
                            subst assm_ts orig_t =
   let
@@ -333,7 +329,6 @@
     val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
     val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
     val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
-    val _ = List.app check_constr_nut need_us
     val (free_names, const_names) =
       fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
     val (sel_names, nonsel_names) =
diff -r e5dba3d75e9e -r 09b75d55008f src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 15 13:03:54 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 15 15:49:42 2011 +0100
@@ -1506,8 +1506,7 @@
                      end
                  else
                    accum)
-        | aux u =
-          raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
+        | aux _ = I
     in
       case SOME (index_seq 0 card, []) |> fold aux need_us of
         SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)