--- a/src/Pure/Isar/outer_syntax.ML Thu Sep 22 00:12:17 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 22 11:25:27 2016 +0200
@@ -220,17 +220,17 @@
in
-fun parse thy pos str =
- Source.of_string str
- |> Symbol.source
- |> Token.source (Thy_Header.get_keywords thy) pos
- |> commands_source thy
- |> Source.exhaust;
+fun parse thy pos =
+ Symbol.explode
+ #> Source.of_list
+ #> Token.source (Thy_Header.get_keywords thy) pos
+ #> commands_source thy
+ #> Source.exhaust;
-fun parse_tokens thy toks =
- Source.of_list toks
- |> commands_source thy
- |> Source.exhaust;
+fun parse_tokens thy =
+ Source.of_list
+ #> commands_source thy
+ #> Source.exhaust;
end;