src/HOL/Tools/Nitpick/nitpick_model.ML

           HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
         else if T = @{typ bisim_iterator} then
           HOLogic.mk_number nat_T j
         else case datatype_spec datatypes T of
           NONE => atom for_auto T j
-        | SOME {constrs, co, ...} =>
+        | SOME {shallow = true, ...} => atom for_auto T j
+        | SOME {co, constrs, ...} =>
           let
             (* styp -> int list *)
             fun tuples_for_const (s, T) =
               tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
             (* unit -> indexname * typ *)

                     (index_seq 0 card) @
                 (if precise then [] else [Pretty.str unrep]))])
     (* typ -> dtype_spec list *)
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
-        precise = false, constrs = []}]
+        precise = false, shallow = false, constrs = []}]
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
-      List.partition #co datatypes
-      ||> append (integer_datatype nat_T @ integer_datatype int_T)
+      datatypes |> filter_out #shallow
+                |> List.partition #co
+                ||> append (integer_datatype nat_T @ integer_datatype int_T)
     val block_of_datatypes =
       if show_datatypes andalso not (null datatypes) then
         [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
                          (map pretty_for_datatype datatypes)]
       else