src/Pure/Isar/token.ML
changeset 74174 a3b0fc510705
parent 74171 a9e79c3645c4
child 74175 53e28c438f96
--- a/src/Pure/Isar/token.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 23 14:24:57 2021 +0200
@@ -381,7 +381,7 @@
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
-    val end_pos = Position.advance_symbol_explode text (#pos file);
+    val end_pos = Position.symbol_explode text (#pos file);
   in Input.source true text (Position.range (#pos file, end_pos)) end;
 
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files