--- 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
--- 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) =
--- 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)