# HG changeset patch
# User wenzelm
# Date 1377033630 -7200
# Node ID d9ba3417cb41d93801a1b8bdc525c40b7f34317f
# Parent  04d8af9ff64b7d8d2a38e4288ac03fed7ea48562
more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;

diff -r 04d8af9ff64b -r d9ba3417cb41 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Aug 20 21:17:39 2013 +0200
+++ b/src/Pure/Isar/args.ML	Tue Aug 20 23:20:30 2013 +0200
@@ -225,17 +225,25 @@
 
 (* arguments within outer syntax *)
 
+val argument_kinds =
+ [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
+  Token.Nat, Token.Float, Token.String, Token.AltString, Token.Verbatim];
+
 fun parse_args is_symid =
   let
-    val keyword_symid = token (Parse.keyword_with is_symid);
-    fun atom blk = Parse.group (fn () => "argument")
-      (ident || keyword_symid || string || alt_string || token Parse.float_number ||
-        (if blk then token (Parse.$$$ ",") else Scan.fail));
+    fun argument blk =
+      Parse.group (fn () => "argument")
+        (Scan.one (fn tok =>
+          let val kind = Token.kind_of tok in
+            member (op =) argument_kinds kind orelse
+            Token.keyword_with is_symid tok orelse
+            (blk andalso Token.keyword_with (fn s => s = ",") tok)
+          end));
 
     fun args blk x = Scan.optional (args1 blk) [] x
     and args1 blk x =
       ((Scan.repeat1
-        (Scan.repeat1 (atom blk) ||
+        (Scan.repeat1 (argument blk) ||
           argsp "(" ")" ||
           argsp "[" "]")) >> flat) x
     and argsp l r x =