# HG changeset patch
# User wenzelm
# Date 1727468080 -7200
# Node ID e38c65002f44f916a1a041d095a8cc491f5d10fe
# Parent  5e2b1588c5cb141490a7c4336f9cb8332c4fd25c
clarified signature;

diff -r 5e2b1588c5cb -r e38c65002f44 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Sep 27 22:08:54 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Sep 27 22:14:40 2024 +0200
@@ -34,7 +34,7 @@
   val literal: string -> token
   val is_literal: token -> bool
   val token_ord: token ord
-  val tokens_match_ord: token ord
+  val token_type_ord: token ord
   val mk_eof: Position.T -> token
   val eof: token
   val is_eof: token -> bool
@@ -168,7 +168,7 @@
       | ord => ord)
   | ord => ord);
 
-fun tokens_match_ord toks =
+fun token_type_ord toks =
   let val is = apply2 index_of_token toks in
     (case int_ord is of
       EQUAL => if #1 is = literal_index then fast_string_ord (apply2 str_of_token toks) else EQUAL
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;