| changeset 70586 | 57df8a85317a |
| parent 69891 | def3ec9cdb7e |
| child 73163 | 624c2b98860a |
--- a/src/Pure/Syntax/lexicon.ML Tue Aug 20 09:48:22 2019 +0200 +++ b/src/Pure/Syntax/lexicon.ML Tue Aug 20 11:01:05 2019 +0200 @@ -32,7 +32,7 @@ val dummy: token val literal: string -> token val is_literal: token -> bool - val tokens_match_ord: token * token -> order + val tokens_match_ord: token ord val mk_eof: Position.T -> token val eof: token val is_eof: token -> bool