| changeset 74171 | a9e79c3645c4 |
| parent 67522 | 9e712280cc37 |
| child 74174 | a3b0fc510705 |
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML Mon Aug 23 12:25:55 2021 +0200 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Mon Aug 23 12:54:28 2021 +0200 @@ -82,7 +82,7 @@ fun symbol (x : string, _ : Position.T) = x; fun explode_pos s pos = fst (fold_map (fn x => fn pos => - ((x, pos), Position.advance x pos)) (raw_explode s) pos); + ((x, pos), Position.advance_symbol x pos)) (raw_explode s) pos); (** scanners **)