src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 34123 c4988215a691
parent 34121 5e831d805118
child 34124 c4628a1dcf75
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:31:00 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 16:48:49 2009 +0100
     1.3 @@ -238,7 +238,7 @@
     1.4                                    [T1, T1 --> T2] ---> T1 --> T2)
     1.5          (* (term * term) list -> term *)
     1.6          fun aux [] =
     1.7 -            if maybe_opt andalso not (is_precise_type datatypes T1) then
     1.8 +            if maybe_opt andalso not (is_complete_type datatypes T1) then
     1.9                insert_const $ Const (unrep, T1) $ empty_const
    1.10              else
    1.11                empty_const
    1.12 @@ -262,7 +262,7 @@
    1.13                 Const (@{const_name None}, _) => aux' ps
    1.14               | _ => update_const $ aux' ps $ t1 $ t2)
    1.15          fun aux ps =
    1.16 -          if not (is_precise_type datatypes T1) then
    1.17 +          if not (is_complete_type datatypes T1) then
    1.18              update_const $ aux' ps $ Const (unrep, T1)
    1.19              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    1.20            else
    1.21 @@ -601,17 +601,17 @@
    1.22               Pretty.str oper, Syntax.pretty_term ctxt t2])
    1.23        end
    1.24      (* dtype_spec -> Pretty.T *)
    1.25 -    fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) =
    1.26 +    fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
    1.27        Pretty.block (Pretty.breaks
    1.28            [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=",
    1.29             Pretty.enum "," "{" "}"
    1.30                 (map (Syntax.pretty_term ctxt o nth_value_of_type typ card)
    1.31                      (index_seq 0 card) @
    1.32 -                (if precise then [] else [Pretty.str unrep]))])
    1.33 +                (if complete then [] else [Pretty.str unrep]))])
    1.34      (* typ -> dtype_spec list *)
    1.35      fun integer_datatype T =
    1.36        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.37 -        precise = false, shallow = false, constrs = []}]
    1.38 +        complete = false, concrete = true, shallow = false, constrs = []}]
    1.39        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.40      val (codatatypes, datatypes) =
    1.41        datatypes |> filter_out #shallow