src/Pure/library.ML
changeset 35976 ea3d4691a8c6
parent 34059 f3f0e20923a7
child 36692 54b64d4ad524
--- 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 *)