src/Pure/Syntax/lexicon.ML

   val explode_xstr: string -> string list
   val scan_id: string list -> string * string list
   val scan_longid: string list -> string * string list
   val scan_var: string list -> string * string list
   val scan_tid: string list -> string * string list
+  val scan_tvar: string list -> string * string list
   val scan_nat: string list -> string * string list
   val scan_int: string list -> string * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
   val indexname: string list -> indexname

 val scan_nat = scan_digits1 >> implode;
 val scan_int = $$ "~" ^^ scan_nat || scan_nat;
 
 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
 val scan_var = $$ "?" ^^ scan_id_nat;
+val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
 
 
 
 (** string_of_vname **)
 

     val scan_xid =
       if xids then $$ "_" ^^ scan_id || scan_id
       else scan_id;
 
     val scan_val =
-      $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy ||
+      scan_tvar >> pair TVarSy ||
       scan_var >> pair VarSy ||
       scan_tid >> pair TFreeSy ||
       $$ "#" ^^ scan_int >> pair NumSy ||		(* FIXME remove "#" *)
       scan_longid >> pair LongIdentSy ||
       scan_xid >> pair IdentSy;