merged

--- a/src/Pure/Isar/args.ML	Tue Aug 20 22:24:02 2013 +0200
+++ b/src/Pure/Isar/args.ML	Tue Aug 20 23:40:23 2013 +0200
@@ -101,7 +101,8 @@
     | Token.Typ T => Token.Typ (Morphism.typ phi T)
     | Token.Term t => Token.Term (Morphism.term phi t)
     | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
-    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
+    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
+    | tok as Token.Files _ => tok));
 
 val assignable = map_args Token.assignable;
 val closure = map_args Token.closure;
@@ -224,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 =

--- a/src/Pure/Isar/bundle.ML	Tue Aug 20 22:24:02 2013 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Aug 20 23:40:23 2013 +0200
@@ -61,7 +61,7 @@
   let
     val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
     val bundle0 = raw_bundle
-      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
+      |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
       Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);