diff -r 7b7109f22224 -r 05b5995f214e src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Aug 18 16:02:11 2004 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Wed Aug 18 16:03:15 2004 +0200
@@ -10,7 +10,7 @@
   datatype token_kind =
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | String | Verbatim | Space | Comment | Sync | Malformed | EOF
-  type token
+  eqtype token
   val str_of_kind: token_kind -> string
   val stopper: token * (token -> bool)
   val not_sync: token -> bool