changeset 63936 | b87784e19a77 |
parent 63640 | c273583f0203 |
child 64421 | 681fae6b00b5 |
--- 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;