# HG changeset patch
# User blanchet
# Date 1298911990 -3600
# Node ID 37ce158d62667ff15640f257fcb6da6b146bef2e
# Parent  07573743208f1e8b21d9ebbed1d8b2c072a3146c
if "total_consts" is set, report cex's as quasi-genuine

diff -r 07573743208f -r 37ce158d6266 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 28 17:53:10 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 28 17:53:10 2011 +0100
@@ -489,7 +489,7 @@
                                     string_of_int j0))
                          (Typtab.dest ofs)
 *)
-        val total_consts =
+        val effective_total_consts =
           case total_consts of
             SOME b => b
           | NONE => forall (is_exact_type datatypes true) all_Ts
@@ -505,7 +505,8 @@
                                     NameTable.empty
         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
         val (nonsel_names, rep_table) =
-          choose_reps_for_consts scope total_consts nonsel_names rep_table
+          choose_reps_for_consts scope effective_total_consts nonsel_names
+                                 rep_table
         val (guiltiest_party, min_highest_arity) =
           NameTable.fold (fn (name, R) => fn (s, n) =>
                              let val n' = arity_of_rep R in
@@ -642,7 +643,8 @@
               nonsel_names rel_table bounds
         val genuine_means_genuine =
           got_all_user_axioms andalso none_true wfs andalso
-          sound_finitizes andalso codatatypes_ok
+          sound_finitizes andalso total_consts <> SOME true andalso
+          codatatypes_ok
         fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
       in
         (pprint (Pretty.chunks
@@ -698,6 +700,8 @@
                           ? cons ("wf", "\"smart\" or \"false\"")
                        |> not sound_finitizes
                           ? cons ("finitize", "\"smart\" or \"false\"")
+                       |> total_consts = SOME true
+                          ? cons ("total_consts", "\"smart\" or \"false\"")
                        |> not codatatypes_ok
                           ? cons ("bisim_depth", "a nonnegative value")
                   val ss =