exported explicit equality on tokens
authorhaftmann
Wed Dec 27 16:24:31 2006 +0100 (2006-12-27)
changeset 21903bb5b9c267c1d
parent 21902 8e5e2571c716
child 21904 59fcfa2a77ea
exported explicit equality on tokens
src/Pure/Isar/outer_lex.ML
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Wed Dec 27 16:18:07 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Wed Dec 27 16:24:31 2006 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     1.5      Nat | String | AltString | Verbatim | Space | Comment | Sync | Malformed | EOF
     1.6    eqtype token
     1.7 +  val eq_token: token * token -> bool
     1.8    val str_of_kind: token_kind -> string
     1.9    val stopper: token * (token -> bool)
    1.10    val not_sync: token -> bool
    1.11 @@ -80,6 +81,7 @@
    1.12    | Malformed => "bad input"
    1.13    | EOF => "end-of-file";
    1.14  
    1.15 +val eq_token = op = : token * token -> bool;
    1.16  
    1.17  (* control tokens *)
    1.18