# HG changeset patch
# User wenzelm
# Date 1116346240 -7200
# Node ID 35ec4802c66c0481320b330953cdf3926c11cb98
# Parent  db3cd4fa9b19f92720dba93e92c8492b1c90a44e
Syntax.read_variable;

diff -r db3cd4fa9b19 -r 35ec4802c66c src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue May 17 18:10:39 2005 +0200
+++ b/src/Pure/Isar/args.ML	Tue May 17 18:10:40 2005 +0200
@@ -251,10 +251,7 @@
 
 val nat = some_ident Syntax.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
-
-(*variable name; leading '?' may be omitted if name contains no dot*)
-val read_var = try (#1 o Term.dest_Var o Syntax.read_var);
-val var = some_ident read_var || some_ident (fn x => read_var ("?" ^ x));
+val var = some_ident Syntax.read_variable;
 
 
 (* enumerations *)
@@ -399,4 +396,3 @@
       [Pretty.enclose "[" "]" (Pretty.commas (map (pretty_src ctxt) srcs))];
 
 end;
-