diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/Isar/parse.ML Sun Oct 24 16:43:54 2021 +0200 @@ -517,7 +517,7 @@ fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper; fun read_antiq keywords scan (syms, pos) = - (case Scan.read Token.stopper scan (tokenize (Keyword.no_command_keywords keywords) syms) of + (case Scan.read Token.stopper scan (tokenize (Keyword.no_major_keywords keywords) syms) of SOME res => res | NONE => error ("Malformed antiquotation" ^ Position.here pos));