src/HOL/Tools/Nitpick/nitpick.ML
changeset 41985 09b75d55008f
parent 41944 b97091ae583a
child 41992 0e4716fa330a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 13:03:54 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 15:49:42 2011 +0100
     1.3 @@ -197,10 +197,6 @@
     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 \"need\" 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 @@ -333,7 +329,6 @@
    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 need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
    1.18 -    val _ = List.app check_constr_nut need_us
    1.19      val (free_names, const_names) =
    1.20        fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
    1.21      val (sel_names, nonsel_names) =