diff -r 389f315f8c24 -r 08e0d3f248f9 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 00:26:14 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 11:50:20 2024 +0200
@@ -174,14 +174,6 @@
 
     val markup_cache = markup_entity_cache ctxt;
 
-    fun report_literals a ts = List.app (report_literal a) ts
-    and report_literal a t =
-      (case t of
-        Parser.Markup (_, ts) => report_literals a ts
-      | Parser.Node _ => ()
-      | Parser.Tip tok =>
-          if Lexicon.is_literal tok then report (report_pos tok) markup_cache a else ());
-
     val ast_of_pos = Ast.Variable o Term_Position.encode;
     val ast_of_position = ast_of_pos o single o report_pos;
     fun ast_of_position' a = Ast.constrain (Ast.Constant a) o ast_of_position;