# HG changeset patch
# User haftmann
# Date 1167233071 -3600
# Node ID bb5b9c267c1dc06c83ebf9d81a46328100914ee2
# Parent  8e5e2571c71660e8f455d37f5caccd4d6f1d973f
exported explicit equality on tokens

diff -r 8e5e2571c716 -r bb5b9c267c1d src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Dec 27 16:18:07 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Wed Dec 27 16:24:31 2006 +0100
@@ -11,6 +11,7 @@
     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
@@ -80,6 +81,7 @@
   | Malformed => "bad input"
   | EOF => "end-of-file";
 
+val eq_token = op = : token * token -> bool;
 
 (* control tokens *)