diff -r 422024102d9d -r 8bedca4bd5a3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -118,12 +118,7 @@
 (* check *)
 
 fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
-
-fun check_src_generic context src =
-  let
-    val ((xname, toks), pos) = Args.dest_src src;
-    val name = check_name_generic context (xname, pos);
-  in Args.src ((name, toks), pos) end;
+fun check_src_generic context src = #1 (Args.check_src context (get_attributes context) src);
 
 val check_name = check_name_generic o Context.Proof;
 val check_src = check_src_generic o Context.Proof;
@@ -141,13 +136,8 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val table = get_attributes context in
-    fn src =>
-      let
-        val ((name, _), _) = Args.dest_src src;
-        val (att, _) = Name_Space.get table name;
-      in att src end
-  end;
+  let val table = get_attributes context
+  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;
@@ -201,7 +191,7 @@
 
 (* internal attribute *)
 
-fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
+fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
 
 val _ = Theory.setup
  (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
@@ -273,7 +263,7 @@
   in (src2, result) end;
 
 fun err msg src =
-  let val ((name, _), pos) = Args.dest_src src
+  let val (name, pos) = Args.name_of_src src
   in error (msg ^ " " ^ quote name ^ Position.here pos) end;
 
 fun eval src ((th, dyn), (decls, context)) =