diff -r 7120ef5bc378 -r edab0ecfbd7c src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sat Dec 30 16:08:05 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Sat Dec 30 16:08:06 2006 +0100
@@ -11,7 +11,6 @@
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | String | AltString | Verbatim | Space | Comment | Sync | Malformed | EOF
   eqtype token
-  val eq_token: token * token -> bool
   val str_of_kind: token_kind -> string
   val stopper: token * (token -> bool)
   val not_sync: token -> bool
@@ -62,8 +61,6 @@
 
 datatype token = Token of Position.T * (token_kind * string);
 
-val eq_token = op = : token * token -> bool;
-
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"