diff -r 17909568216e -r 57df8a85317a src/Pure/Syntax/lexicon.ML
--- 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