diff -r d492b2ab7351 -r 8fbccead3695 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu May 07 18:05:08 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu May 07 18:05:46 1998 +0200
@@ -14,6 +14,7 @@
   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
@@ -93,6 +94,7 @@
 
 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
 val scan_var = $$ "?" ^^ scan_id_nat;
+val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
 
 
 
@@ -246,7 +248,7 @@
       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 "#" *)