tuned white space;

--- 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 *)