clarified;

--- a/src/Pure/General/antiquote.ML	Wed Oct 14 15:10:32 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Wed Oct 14 17:24:03 2015 +0200
@@ -42,7 +42,7 @@
           | ([], _ :: rest) => flush #> split (Text rest)
           | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest))
       | split a = add a;
-  in rev (#2 (flush (fold split input ([], [])))) end;
+  in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end;
 
 
 (* reports *)