# HG changeset patch
# User wenzelm
# Date 1444836243 -7200
# Node ID 8626c2fed037dad8033f550f38c01e298cbc844a
# Parent  2bf52eec4e8ac0c061f70cc2400ce3a4cc3dfeb1
clarified;

diff -r 2bf52eec4e8a -r 8626c2fed037 src/Pure/General/antiquote.ML
--- 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 *)