diff -r 6d0c1b2dc717 -r 6bce9ef27d7e src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Jan 30 11:01:49 1998 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Jan 30 11:31:21 1998 +0100
@@ -52,6 +52,7 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
+  val read_var: string -> string * int
 end;
 
 signature LEXICON =
@@ -493,4 +494,13 @@
   end;
 
 
+(* read_var *)
+
+fun read_var str =
+  let val scan = $$ "?" -- scan_vname -- scan_end >> (#2 o #1) in
+    #1 (scan (explode str)) handle LEXICAL_ERROR
+      => error ("Bad variable " ^ quote str)
+  end;
+
+
 end;