src/Pure/Syntax/syntax_phases.ML
changeset 81009 719a02488d25
parent 81008 d0cd220d8e8b
child 81016 8e2114e6205b
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 21:16:17 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 21:20:36 2024 +0200
@@ -165,7 +165,7 @@
     and report_literal a t =
       (case t of
         Parser.Markup (_, ts) => report_literals a ts
-      | Parser.Node ({const, ...}, ts) => if const = "" then report_literals a ts else ()
+      | Parser.Node _ => ()
       | Parser.Tip tok =>
           if Lexicon.is_literal tok then report (report_pos tok) (markup_entity ctxt) a else ());