diff -r 88dbcfe75c45 -r 29f81babefd7 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 10:08:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 25 16:33:39 2010 +0100
@@ -288,7 +288,7 @@
                                   T1 --> (T1 --> T2) --> T1 --> T2)
         (* (term * term) list -> term *)
         fun aux [] =
-            if maybe_opt andalso not (is_complete_type datatypes T1) then
+            if maybe_opt andalso not (is_complete_type datatypes false T1) then
               insert_const $ Const (unrep, T1) $ empty_const
             else
               empty_const
@@ -312,7 +312,7 @@
                Const (@{const_name None}, _) => aux' ps
              | _ => update_const $ aux' ps $ t1 $ t2)
         fun aux ps =
-          if not (is_complete_type datatypes T1) then
+          if not (is_complete_type datatypes false T1) then
             update_const $ aux' ps $ Const (unrep, T1)
             $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
           else
@@ -537,7 +537,7 @@
           val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
           val ts2 =
             map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
-                                       [[int_for_bool (member (op =) jss js)]])
+                                       [[int_from_bool (member (op =) jss js)]])
                 jss1
         in make_fun false T1 T2 T' ts1 ts2 end
       | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
@@ -707,12 +707,13 @@
            Pretty.str "=",
            Pretty.enum "," "{" "}"
                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
-                (if complete then [] else [Pretty.str unrep]))])
+                (if fun_from_pair complete false then []
+                 else [Pretty.str unrep]))])
     (* typ -> dtype_spec list *)
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
-        standard = true, complete = false, concrete = true, deep = true,
-        constrs = []}]
+        standard = true, complete = (false, false), concrete = (true, true),
+        deep = true, constrs = []}]
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
       datatypes |> filter #deep |> List.partition #co