diff -r 0c6a600c8939 -r 1f5462055655 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sun Sep 29 15:24:17 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Sep 29 15:58:28 2024 +0200
@@ -531,8 +531,8 @@
     if pointer_eq arg then EQUAL
     else
       (case apply2 drop_markup arg of
-        (Node_Op ({const = s, ...}, ts) :: rest, Node_Op ({const = s', ...}, ts') :: rest') =>
-          (case fast_string_ord (s, s') of
+        (Node_Op ({nonterm = nt, ...}, ts) :: rest, Node_Op ({nonterm = nt', ...}, ts') :: rest') =>
+          (case int_ord (nt, nt') of
             EQUAL =>
               (case tree_ops_ord (ts, ts') of
                 EQUAL => tree_ops_ord (rest, rest')