src/HOL/Tools/ATP/atp_problem_generate.ML

               else
                 NONE
           end
         fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
           let val ctrs' = map do_ctr ctrs in
-            (native_ho_type_of_typ type_enc false 0 (body_type T1),
-             map_filter I ctrs', forall is_some ctrs')
+            if forall is_some ctrs' then
+              SOME (native_ho_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
+            else
+              NONE
           end
-      in ctrss |> map datatype_of_ctrs |> filter_out (null o #2) end
+      in
+        map_filter datatype_of_ctrs ctrss
+      end
     else
       []
   | datatypes_of_sym_table _ _ _ _ _ _ = []
 
-fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs, exhaust) =
+fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
   let val xs = map (fn AType (name, []) => name) ty_args in
-    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
-                   ctrs, exhaust)
+    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
   end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
 fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab

       | do_formula (AConn (_, phis)) = fold do_formula phis
       | do_formula (AAtom tm) = do_term true tm
     fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
       | do_line (Type_Decl _) = I
       | do_line (Sym_Decl (_, _, ty)) = do_type ty
-      | do_line (Datatype_Decl (_, xs, ty, tms, _)) =
+      | do_line (Datatype_Decl (_, xs, ty, tms)) =
         fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
       | do_line (Class_Memb (_, xs, ty, cl)) =
         fold do_bound_tvars xs #> do_type ty #> do_class cl
       | do_line (Formula (_, _, phi, _, _)) = do_formula phi
     val ((cls, tys), syms) = declared_in_atp_problem problem