tuned whitespace;

--- a/src/Pure/library.ML	Thu Dec 13 21:36:09 2018 +0100
+++ b/src/Pure/library.ML	Fri Dec 14 11:35:21 2018 +0100
@@ -599,6 +599,7 @@
 fun suffixes xs = [] :: suffixes1 xs;
 
 
+
 (** integers **)
 
 (* lists of integers *)
@@ -794,6 +795,7 @@
   in match (space_explode "*" pat) str end;
 
 
+
 (** reals **)
 
 val string_of_real = Real.fmt (StringCvt.GEN NONE);