src/Pure/General/symbol_pos.ML
changeset 62239 6ee95b93fbed
parent 62210 e068ea693678
child 62529 8b7bdfc09f3b
--- a/src/Pure/General/symbol_pos.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -71,7 +71,7 @@
         fun split syms =
           (case take_prefix (fn (s, _) => s <> "\n") syms of
             (line, []) => [line]
-          | (line, nl :: rest) => line :: split rest);
+          | (line, _ :: rest) => line :: split rest);
       in split list end;
 
 val trim_blanks = trim (Symbol.is_blank o symbol);