src/Pure/Syntax/lexicon.ML

 signature LEXICON =
 sig
   include SCANNER
   include LEXICON0
   val is_xid: string -> bool
-  val is_tfree: string -> bool
+  val is_tid: string -> bool
   type lexicon
   datatype token =
     Token of string |
     IdentSy of string |
     VarSy of string |
     TFreeSy of string |
     TVarSy of string |
     EndToken
   val id: string
   val var: string
-  val tfree: string
+  val tid: string
   val tvar: string
   val terminals: string list
   val is_terminal: string -> bool
   val str_of_token: token -> string
   val display_token: token -> string
   val matching_tokens: token * token -> bool
+  val token_assoc: (token option * 'a list) list * token -> 'a list
   val valued_token: token -> bool
   val predef_term: string -> token option
   val dest_lexicon: lexicon -> string list
   val empty_lexicon: lexicon
   val extend_lexicon: lexicon -> string list -> lexicon

 fun is_xid s =
   (case explode s of
     "_" :: cs => is_ident cs
   | cs => is_ident cs);
 
-fun is_tfree s =
+fun is_tid s =
   (case explode s of
     "'" :: cs => is_ident cs
   | _ => false);
 
 

 
 (* terminal arguments *)
 
 val id = "id";
 val var = "var";
-val tfree = "tfree";
+val tid = "tid";
 val tvar = "tvar";
 
-val terminals = [id, var, tfree, tvar];
+val terminals = [id, var, tid, tvar];
 
 fun is_terminal s = s mem terminals;
 
 
 (* str_of_token *)

 (* display_token *)
 
 fun display_token (Token s) = quote s
   | display_token (IdentSy s) = "id(" ^ s ^ ")"
   | display_token (VarSy s) = "var(" ^ s ^ ")"
-  | display_token (TFreeSy s) = "tfree(" ^ s ^ ")"
+  | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
   | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
   | display_token EndToken = "";
 
 
 (* matching_tokens *)

   | matching_tokens (TVarSy _, TVarSy _) = true
   | matching_tokens (EndToken, EndToken) = true
   | matching_tokens _ = false;
 
 
+(* this function is needed in parser.ML but is placed here 
+   for better performance *)
+fun token_assoc (list, key) =
+  let fun assoc [] = []
+        | assoc ((keyi, xi) :: pairs) =
+            if is_none keyi orelse matching_tokens (the keyi, key) then 
+              (assoc pairs) @ xi
+            else assoc pairs;
+  in assoc list end;
+
+
 (* valued_token *)
 
 fun valued_token (Token _) = false
   | valued_token (IdentSy _) = true
   | valued_token (VarSy _) = true

 (* predef_term *)
 
 fun predef_term name =
   if name = id then Some (IdentSy name)
   else if name = var then Some (VarSy name)
-  else if name = tfree then Some (TFreeSy name)
+  else if name = tid then Some (TFreeSy name)
   else if name = tvar then Some (TVarSy name)
   else None;