# HG changeset patch
# User blanchet
# Date 1299067797 -3600
# Node ID a4fb98eb0edf7b72aa3e4535923cd11575d8743c
# Parent  cbfba0453b469f25458b9cf8c511cf16c2aece5f
make "preconstr" option more robust -- shouldn't throw exceptions

diff -r cbfba0453b46 -r a4fb98eb0edf src/HOL/Tools/Nitpick/nitpick.ML
--- 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) =