# HG changeset patch
# User blanchet
# Date 1266006426 -3600
# Node ID 29a0e3be0be1ec1284ddfeb3a9b61d09a1fe9b26
# Parent  168041f24f8082f97b2cf1307aaae54d27a4ba04
minor fixes to Nitpick

diff -r 168041f24f80 -r 29a0e3be0be1 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Fri Feb 12 19:44:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 12 21:27:06 2010 +0100
@@ -1369,7 +1369,7 @@
 
 \prew
 \slshape
-Hint: To check that the induction hypothesis is general enough, try the following command:
+Hint: To check that the induction hypothesis is general enough, try this command:
 \textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
 \postw
 
diff -r 168041f24f80 -r 29a0e3be0be1 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 12 19:44:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 12 21:27:06 2010 +0100
@@ -317,7 +317,8 @@
              [ts] |> not exclusive ? cons (KK.TupleSet [])
            else
              [KK.TupleSet [],
-              if T1 = T2 andalso epsilon > delta then
+              if T1 = T2 andalso epsilon > delta andalso
+                 not (datatype_spec dtypes T1 |> the |> #co) then
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
                            KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
@@ -833,7 +834,7 @@
 (* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
    -> constr_spec -> int -> KK.formula *)
 fun sel_axiom_for_sel hol_ctxt j0
-        (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
+        (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
                 kk_join, ...}) rel_table dom_r
         ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
         n =
@@ -864,19 +865,19 @@
       [formula_for_bool honors_explicit_max]
     else
       let
-        val ran_r = discr_rel_expr rel_table const
+        val dom_r = discr_rel_expr rel_table const
         val max_axiom =
           if honors_explicit_max then
             KK.True
           else if is_twos_complement_representable bits (epsilon - delta) then
-            KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
+            KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
           else
             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
                              "\"bits\" value " ^ string_of_int bits ^
                              " too small for \"max\"")
       in
         max_axiom ::
-        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
+        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
             (index_seq 0 (num_sels_for_constr_type (snd const)))
       end
   end
diff -r 168041f24f80 -r 29a0e3be0be1 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 19:44:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 21:27:06 2010 +0100
@@ -162,7 +162,7 @@
     fun miscs () =
       (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
-       else ["bisim_depth = " ^ string_of_int bisim_depth])
+       else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
   in
     setmp_show_all_types
         (fn () => (cards primary_card_assigns, cards secondary_card_assigns,