src/HOL/Tools/Nitpick/nitpick.ML
changeset 41876 03f699556955
parent 41875 e3cd0dce9b1a
child 41888 79f837c2e33b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
     1.3 @@ -35,7 +35,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       peephole_optim: bool,
    1.10       datatype_sym_break: int,
    1.11       kodkod_sym_break: int,
    1.12 @@ -110,7 +110,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     peephole_optim: bool,
    1.19     datatype_sym_break: int,
    1.20     kodkod_sym_break: int,
    1.21 @@ -258,7 +258,7 @@
    1.22                       o Date.fromTimeLocal o Time.now)
    1.23      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    1.24                  else orig_t
    1.25 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    1.26 +    val conj_ts = neg_t :: assm_ts @ evals @ these needs
    1.27      val tfree_table =
    1.28        if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
    1.29        else []
    1.30 @@ -266,8 +266,8 @@
    1.31      val neg_t = neg_t |> merge_tfrees
    1.32      val assm_ts = assm_ts |> map merge_tfrees
    1.33      val evals = evals |> map merge_tfrees
    1.34 -    val needs = needs |> map (apfst (Option.map merge_tfrees))
    1.35 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    1.36 +    val needs = needs |> Option.map (map merge_tfrees)
    1.37 +    val conj_ts = neg_t :: assm_ts @ evals @ these needs
    1.38      val original_max_potential = max_potential
    1.39      val original_max_genuine = max_genuine
    1.40      val max_bisim_depth = fold Integer.max bisim_depths ~1