diff -r 5e2b1588c5cb -r e38c65002f44 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 22:08:54 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 22:14:40 2024 +0200
@@ -51,7 +51,7 @@
 
 (* tokens *)
 
-structure Tokens = Set(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
+structure Tokens = Set(type key = Lexicon.token val ord = Lexicon.token_type_ord);
 
 fun tokens_find P tokens = Tokens.get_first (fn tok => if P tok then SOME tok else NONE) tokens;
 fun tokens_add (nt: nt, tokens) = if Tokens.is_empty tokens then I else cons (nt, tokens);
@@ -631,7 +631,7 @@
               let
                 val (_, _, id, _) = info;
                 val Sii' =
-                  if Lexicon.tokens_match_ord (a, c) <> EQUAL then Sii
+                  if Lexicon.token_type_ord (a, c) <> EQUAL then Sii
                   else (*move dot*)
                     let val ts' = if Lexicon.valued_token c orelse id <> "" then Tip c :: ts else ts
                     in (info, sa, ts') :: Sii end;