src/HOL/Tools/record_package.ML

         [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)];
 
       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
           pretty_parent parent @ map pretty_field fields));
-    in seq (Pretty.writeln o pretty_record) (Sign.cond_extern_table sg Sign.typeK recs) end;
+    in
+      map pretty_record (Sign.cond_extern_table sg Sign.typeK recs)
+      |> Pretty.chunks |> Pretty.writeln
+    end;
 end;
 
 structure RecordsData = TheoryDataFun(RecordsArgs);
 val print_records = RecordsData.print;