diff -r aa1fe1103ab8 -r b87784e19a77 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Sep 22 00:12:17 2016 +0200
+++ b/src/Pure/Isar/token.ML	Thu Sep 22 11:25:27 2016 +0200
@@ -650,8 +650,8 @@
 (* explode *)
 
 fun explode keywords pos =
-  Source.of_string #>
-  Symbol.source #>
+  Symbol.explode #>
+  Source.of_list #>
   source keywords pos #>
   Source.exhaust;