src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35220 2bcdae5f4fdb
parent 35190 ce653cc27a94
child 35280 54ab4921f826
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 10:38:37 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 18:48:07 2010 +0100
     1.3 @@ -264,8 +264,8 @@
     1.4     -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
     1.5     -> typ -> rep -> int list list -> term *)
     1.6  fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
     1.7 -        ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
     1.8 -          ofs, ...} : scope) sel_names rel_table bounds =
     1.9 +        ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
    1.10 +          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
    1.11    let
    1.12      val for_auto = (maybe_name = "")
    1.13      (* int list list -> int *)
    1.14 @@ -388,7 +388,7 @@
    1.15          if j = 0 then @{const False} else @{const True}
    1.16        | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
    1.17        | term_for_atom seen T _ j k =
    1.18 -        if T = nat_T then
    1.19 +        if T = nat_T andalso is_standard_datatype thy stds nat_T then
    1.20            HOLogic.mk_number nat_T j
    1.21          else if T = int_T then
    1.22            HOLogic.mk_number int_T (int_for_atom (k, 0) j)
    1.23 @@ -713,7 +713,9 @@
    1.24        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.25      val (codatatypes, datatypes) =
    1.26        datatypes |> filter #deep |> List.partition #co
    1.27 -                ||> append (integer_datatype nat_T @ integer_datatype int_T)
    1.28 +                ||> append (integer_datatype int_T
    1.29 +                            |> is_standard_datatype thy stds nat_T
    1.30 +                               ? append (integer_datatype nat_T))
    1.31      val block_of_datatypes =
    1.32        if show_datatypes andalso not (null datatypes) then
    1.33          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")