src/HOL/Tools/datatype_case.ML

     val originals = map (row_of_pat o #2) rows
     val _ = case originals \\ finals of
         [] => ()
       | is => (if err then case_error else warning)
           ("The following clauses are redundant (covered by preceding clauses):\n" ^
-           space_implode "\n" (map (string_of_clause o nth clauses) is));
+           cat_lines (map (string_of_clause o nth clauses) is));
   in
     (case_tm, patts2)
   end;
 
 fun make_case tab ctxt = gen_make_case