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 ());