tuned signature;

--- a/src/Pure/Isar/args.ML	Thu Jun 25 16:14:00 2015 +0200
+++ b/src/Pure/Isar/args.ML	Thu Jun 25 16:56:04 2015 +0200
@@ -21,14 +21,15 @@
   val bracks: 'a parser -> 'a parser
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
+  val name_token: Token.T parser
+  val name_inner_syntax: string parser
+  val name_input: Input.source parser
+  val name: string parser
   val cartouche_inner_syntax: string parser
   val cartouche_input: Input.source parser
   val text_token: Token.T parser
   val text_input: Input.source parser
   val text: string parser
-  val name_inner_syntax: string parser
-  val name_input: Input.source parser
-  val name: string parser
   val binding: binding parser
   val alt_name: string parser
   val symbol: string parser
@@ -92,8 +93,6 @@
       else Scan.fail
     end);
 
-val named = ident || string;
-
 val add = $$$ "add";
 val del = $$$ "del";
 val colon = $$$ ":";
@@ -107,18 +106,19 @@
 fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
+val name_token = ident || string;
+val name_inner_syntax = name_token >> Token.inner_syntax_of;
+val name_input = name_token >> Token.input_of;
+val name = name_token >> Token.content_of;
+
 val cartouche = Parse.token Parse.cartouche;
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
 val cartouche_input = cartouche >> Token.input_of;
 
-val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
+val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
 val text_input = text_token >> Token.input_of;
 val text = text_token >> Token.content_of;
 
-val name_inner_syntax = named >> Token.inner_syntax_of;
-val name_input = named >> Token.input_of;
-
-val name = named >> Token.content_of;
 val binding = Parse.position name >> Binding.make;
 val alt_name = alt_string >> Token.content_of;
 val symbol = symbolic >> Token.content_of;
@@ -144,19 +144,22 @@
 val internal_attribute = value (fn Token.Attribute att => att);
 val internal_declaration = value (fn Token.Declaration decl => decl);
 
-fun named_source read = internal_source || named >> evaluate Token.Source read;
+fun named_source read = internal_source || name_token >> evaluate Token.Source read;
 
-fun named_typ read = internal_typ || named >> evaluate Token.Typ (read o Token.inner_syntax_of);
-fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
+fun named_typ read =
+  internal_typ || name_token >> evaluate Token.Typ (read o Token.inner_syntax_of);
+
+fun named_term read =
+  internal_term || name_token >> evaluate Token.Term (read o Token.inner_syntax_of);
 
 fun named_fact get =
   internal_fact ||
-  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
+  name_token >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
   alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
 
 fun named_attribute att =
   internal_attribute ||
-  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
+  name_token >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
 
 fun text_declaration read =
   internal_declaration || text_token >> evaluate Token.Declaration (read o Token.input_of);
@@ -203,7 +206,7 @@
 fun attribs check =
   let
     fun intern tok = check (Token.content_of tok, Token.pos_of tok);
-    val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
+    val attrib_name = internal_name >> #1 || (symbolic || name_token) >> evaluate Token.name0 intern;
     val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;