src/HOL/Tools/Nitpick/nitpick.ML
changeset 41995 03c2d29ec790
parent 41993 bd6296de1432
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 18 10:17:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 18 11:43:28 2011 +0100
     1.3 @@ -564,9 +564,13 @@
     1.4          val plain_rels = free_rels @ other_rels
     1.5          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
     1.6          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
     1.7 -        val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
     1.8 +        val need_vals =
     1.9 +          map (fn dtype as {typ, ...} =>
    1.10 +                  (typ, needed_values_for_datatype need_us ofs dtype)) datatypes
    1.11 +        val sel_bounds =
    1.12 +          map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels
    1.13          val dtype_axioms =
    1.14 -          declarative_axioms_for_datatypes hol_ctxt binarize need_us
    1.15 +          declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
    1.16                datatype_sym_break bits ofs kk rel_table datatypes
    1.17          val declarative_axioms = plain_axioms @ dtype_axioms
    1.18          val univ_card = Int.max (univ_card nat_card int_card main_j0