# HG changeset patch
# User wenzelm
# Date 1517395796 -3600
# Node ID c2151a6bfd5714fdbf2e15b54f787fd7424e52a5
# Parent  77d497947fc773735819a2931b74aca42369740d
more abstract type;

diff -r 77d497947fc7 -r c2151a6bfd57 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:46:55 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:49:56 2018 +0100
@@ -24,7 +24,7 @@
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
     String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
   val token_kind_ord: token_kind * token_kind -> order
-  datatype token = Token of token_kind * string * Position.range
+  eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T