author | wenzelm |
Mon, 30 Sep 2024 12:59:50 +0200 | |
changeset 81017 | bc5eb7841b74 |
parent 81016 | 8e2114e6205b |
child 81018 | 83596aea48cb |
--- a/src/Pure/Syntax/parser.ML Mon Sep 30 11:42:52 2024 +0200 +++ b/src/Pure/Syntax/parser.ML Mon Sep 30 12:59:50 2024 +0200 @@ -574,7 +574,7 @@ | ord => ord) | ord => ord) | (Tip_Op t :: rest, Tip_Op t' :: rest') => - (case Lexicon.token_ord (t, t') of + (case Lexicon.token_content_ord (t, t') of EQUAL => tree_ops_ord (rest, rest') | ord => ord) | (Node_Op _ :: _, Tip_Op _ :: _) => LESS