# HG changeset patch
# User wenzelm
# Date 1544783721 -3600
# Node ID 54a95e1199cb445af17e2e4378d750739d42969f
# Parent  e8893c8932410c0c5230875bd9a23aaf3e8c387c
tuned whitespace;

diff -r e8893c893241 -r 54a95e1199cb src/Pure/library.ML
--- 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);