src/Pure/Thy/thy_syntax.ML

 local
 
 fun reports_of_token keywords tok =
   let
     val malformed_symbols =
-      Input.source_explode (Token.source_position_of tok)
+      Input.source_explode (Token.input_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;