src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35385 29f81babefd7
parent 35280 54ab4921f826
child 35388 42d39948cace
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 10:08:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 16:33:39 2010 +0100
     1.3 @@ -288,7 +288,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_complete_type datatypes T1) then
     1.8 +            if maybe_opt andalso not (is_complete_type datatypes false T1) then
     1.9                insert_const $ Const (unrep, T1) $ empty_const
    1.10              else
    1.11                empty_const
    1.12 @@ -312,7 +312,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_complete_type datatypes T1) then
    1.17 +          if not (is_complete_type datatypes false 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 @@ -537,7 +537,7 @@
    1.22            val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
    1.23            val ts2 =
    1.24              map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
    1.25 -                                       [[int_for_bool (member (op =) jss js)]])
    1.26 +                                       [[int_from_bool (member (op =) jss js)]])
    1.27                  jss1
    1.28          in make_fun false T1 T2 T' ts1 ts2 end
    1.29        | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
    1.30 @@ -707,12 +707,13 @@
    1.31             Pretty.str "=",
    1.32             Pretty.enum "," "{" "}"
    1.33                 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
    1.34 -                (if complete then [] else [Pretty.str unrep]))])
    1.35 +                (if fun_from_pair complete false then []
    1.36 +                 else [Pretty.str unrep]))])
    1.37      (* typ -> dtype_spec list *)
    1.38      fun integer_datatype T =
    1.39        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.40 -        standard = true, complete = false, concrete = true, deep = true,
    1.41 -        constrs = []}]
    1.42 +        standard = true, complete = (false, false), concrete = (true, true),
    1.43 +        deep = true, constrs = []}]
    1.44        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.45      val (codatatypes, datatypes) =
    1.46        datatypes |> filter #deep |> List.partition #co