diff -r e42da880c61e -r 162a4c2e97bc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Nov 11 18:16:25 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Nov 11 20:11:38 2014 +0100
@@ -206,13 +206,12 @@
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
-fun attribute_setup name source cmt =
-  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-    ML_Lex.read_source false source @
-    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+fun attribute_setup name source comment =
+  ML_Lex.read_source false source
   |> ML_Context.expression (#range source)
-    "val (name, scan, comment): binding * attribute context_parser * string"
-    "Context.map_proof (Attrib.local_setup name scan comment)"
+    "val parser: Thm.attribute context_parser"
+    ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+      " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;