# HG changeset patch
# User wenzelm
# Date 1269631805 -3600
# Node ID ea3d4691a8c6e50192ac88236d68147c04bcd676
# Parent  cef3c78ace0adeae6522c51414c11232e535e12d
tuned white space;

diff -r cef3c78ace0a -r ea3d4691a8c6 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Mar 26 20:28:15 2010 +0100
+++ b/src/Pure/library.ML	Fri Mar 26 20:30:05 2010 +0100
@@ -774,6 +774,8 @@
             | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
   in match (space_explode "*" pat) str end;
 
+
+
 (** lists as sets -- see also Pure/General/ord_list.ML **)
 
 (* canonical operations *)