Structure term_tokens

signature term_tokens =
sig

  datatype 'a term_token =
    Ident of string
  | Antiquote of 'a
  | Numeral of (Arbnum.num * char option)
  | Fraction of {wholepart : Arbnum.num, fracpart : Arbnum.num,
                 places : int}
  | QIdent of (string * string)

  val lex : string list -> 'a qbuf.qbuf -> 'a term_token locn.located option
      (* NONE indicates end of input; this function *always* advances over
         what it pulls out of the qbuf.   *)

  val user_split_ident : string list -> string -> (string * string)

  val token_string : 'a term_token -> string
  val dest_aq      : 'a term_token -> 'a
  val is_ident     : 'a term_token -> bool
  val is_aq        : 'a term_token -> bool

  val nonagg_c     : char -> bool

  val lextest : string list -> string -> 'a term_token list

end

HOL 4, Kananaskis-10