1.1 --- a/doc-src/Nitpick/nitpick.tex	Fri Feb 12 19:44:37 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 12 21:27:06 2010 +0100
     1.3 @@ -1369,7 +1369,7 @@
     1.4  
     1.5  \prew
     1.6  \slshape
     1.7 -Hint: To check that the induction hypothesis is general enough, try the following command:
     1.8 +Hint: To check that the induction hypothesis is general enough, try this command:
     1.9  \textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
    1.10  \postw
    1.11  

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 12 19:44:37 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 12 21:27:06 2010 +0100
     2.3 @@ -317,7 +317,8 @@
     2.4               [ts] |> not exclusive ? cons (KK.TupleSet [])
     2.5             else
     2.6               [KK.TupleSet [],
     2.7 -              if T1 = T2 andalso epsilon > delta then
     2.8 +              if T1 = T2 andalso epsilon > delta andalso
     2.9 +                 not (datatype_spec dtypes T1 |> the |> #co) then
    2.10                  index_seq delta (epsilon - delta)
    2.11                  |> map (fn j =>
    2.12                             KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
    2.13 @@ -833,7 +834,7 @@
    2.14  (* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
    2.15     -> constr_spec -> int -> KK.formula *)
    2.16  fun sel_axiom_for_sel hol_ctxt j0
    2.17 -        (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
    2.18 +        (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
    2.19                  kk_join, ...}) rel_table dom_r
    2.20          ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
    2.21          n =
    2.22 @@ -864,19 +865,19 @@
    2.23        [formula_for_bool honors_explicit_max]
    2.24      else
    2.25        let
    2.26 -        val ran_r = discr_rel_expr rel_table const
    2.27 +        val dom_r = discr_rel_expr rel_table const
    2.28          val max_axiom =
    2.29            if honors_explicit_max then
    2.30              KK.True
    2.31            else if is_twos_complement_representable bits (epsilon - delta) then
    2.32 -            KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
    2.33 +            KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
    2.34            else
    2.35              raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
    2.36                               "\"bits\" value " ^ string_of_int bits ^
    2.37                               " too small for \"max\"")
    2.38        in
    2.39          max_axiom ::
    2.40 -        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
    2.41 +        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
    2.42              (index_seq 0 (num_sels_for_constr_type (snd const)))
    2.43        end
    2.44    end

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 19:44:37 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 21:27:06 2010 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4      fun miscs () =
     3.5        (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
     3.6        (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
     3.7 -       else ["bisim_depth = " ^ string_of_int bisim_depth])
     3.8 +       else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
     3.9    in
    3.10      setmp_show_all_types
    3.11          (fn () => (cards primary_card_assigns, cards secondary_card_assigns,