exported explicit equality on tokens
authorhaftmann
Wed, 27 Dec 2006 16:24:31 +0100
changeset 21903 bb5b9c267c1d
parent 21902 8e5e2571c716
child 21904 59fcfa2a77ea
exported explicit equality on tokens
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 *)