--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 01 10:40:14 2011 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 02 13:09:57 2011 +0100
@@ -197,6 +197,10 @@
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 \"preconstr\" 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
@@ -329,6 +333,7 @@
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 preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
+ val _ = List.app check_constr_nut preconstr_us
val (free_names, const_names) =
fold add_free_and_const_names (nondef_us @ def_us) ([], [])
val (sel_names, nonsel_names) =