diff -r 72beac575e9c -r 079fe4292526 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Aug 25 16:00:59 2024 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Aug 25 20:54:20 2024 +0200 @@ -442,7 +442,9 @@ | NONE => Printer.get_binder prtabs c) |> Option.map Prefix); -fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts; +fun is_const (Syntax ({consts, ...}, _)) c = + Graph.defined consts c andalso not (Lexicon.is_marked c); + fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);