src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41876 03f699556955
parent 41875 e3cd0dce9b1a
child 41898 55d981e1232a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4       specialize: bool,
     1.5       star_linear_preds: bool,
     1.6       total_consts: bool option,
     1.7 -     needs: (term option * bool option) list,
     1.8 +     needs: term list option,
     1.9       tac_timeout: Time.time option,
    1.10       evals: term list,
    1.11       case_names: (string * int) list,
    1.12 @@ -261,7 +261,7 @@
    1.13     specialize: bool,
    1.14     star_linear_preds: bool,
    1.15     total_consts: bool option,
    1.16 -   needs: (term option * bool option) list,
    1.17 +   needs: term list option,
    1.18     tac_timeout: Time.time option,
    1.19     evals: term list,
    1.20     case_names: (string * int) list,