make "preconstr" option more robust -- shouldn't throw exceptions
authorblanchet
Wed Mar 02 13:09:57 2011 +0100 (2011-03-02 ago)
changeset 41868a4fb98eb0edf
parent 41867 cbfba0453b46
child 41869 9e367f1c9570
make "preconstr" option more robust -- shouldn't throw exceptions
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 01 10:40:14 2011 +0000
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
     1.3 @@ -197,6 +197,10 @@
     1.4  
     1.5  fun plazy f = Pretty.blk (0, pstrs (f ()))
     1.6  
     1.7 +fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
     1.8 +  | check_constr_nut _ =
     1.9 +    error "The \"preconstr\" option requires a constructor term."
    1.10 +
    1.11  fun pick_them_nits_in_term deadline state (params : params) auto i n step
    1.12                             subst assm_ts orig_t =
    1.13    let
    1.14 @@ -329,6 +333,7 @@
    1.15      val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
    1.16      val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
    1.17      val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
    1.18 +    val _ = List.app check_constr_nut preconstr_us
    1.19      val (free_names, const_names) =
    1.20        fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    1.21      val (sel_names, nonsel_names) =