src/HOL/Tools/Nitpick/nitpick.ML
changeset 41858 37ce158d6266
parent 41856 7244589c8ccc
child 41868 a4fb98eb0edf
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 28 17:53:10 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 28 17:53:10 2011 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4                                      string_of_int j0))
     1.5                           (Typtab.dest ofs)
     1.6  *)
     1.7 -        val total_consts =
     1.8 +        val effective_total_consts =
     1.9            case total_consts of
    1.10              SOME b => b
    1.11            | NONE => forall (is_exact_type datatypes true) all_Ts
    1.12 @@ -505,7 +505,8 @@
    1.13                                      NameTable.empty
    1.14          val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
    1.15          val (nonsel_names, rep_table) =
    1.16 -          choose_reps_for_consts scope total_consts nonsel_names rep_table
    1.17 +          choose_reps_for_consts scope effective_total_consts nonsel_names
    1.18 +                                 rep_table
    1.19          val (guiltiest_party, min_highest_arity) =
    1.20            NameTable.fold (fn (name, R) => fn (s, n) =>
    1.21                               let val n' = arity_of_rep R in
    1.22 @@ -642,7 +643,8 @@
    1.23                nonsel_names rel_table bounds
    1.24          val genuine_means_genuine =
    1.25            got_all_user_axioms andalso none_true wfs andalso
    1.26 -          sound_finitizes andalso codatatypes_ok
    1.27 +          sound_finitizes andalso total_consts <> SOME true andalso
    1.28 +          codatatypes_ok
    1.29          fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
    1.30        in
    1.31          (pprint (Pretty.chunks
    1.32 @@ -698,6 +700,8 @@
    1.33                            ? cons ("wf", "\"smart\" or \"false\"")
    1.34                         |> not sound_finitizes
    1.35                            ? cons ("finitize", "\"smart\" or \"false\"")
    1.36 +                       |> total_consts = SOME true
    1.37 +                          ? cons ("total_consts", "\"smart\" or \"false\"")
    1.38                         |> not codatatypes_ok
    1.39                            ? cons ("bisim_depth", "a nonnegative value")
    1.40                    val ss =