clarified Token.check_src: intern at most once;
Method.parse_internal for Eisbach: intern method names;

--- a/src/Pure/Isar/args.ML	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 10 13:55:10 2015 +0100
@@ -59,6 +59,7 @@
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val attribs: (xstring * Position.T -> string) -> Token.src list parser
   val opt_attribs: (xstring * Position.T -> string) -> Token.src list parser
+  val checked_name: (xstring * Position.T -> string) -> string parser
 end;
 
 structure Args: ARGS =
@@ -209,4 +210,11 @@
 
 fun opt_attribs check = Scan.optional (attribs check) [];
 
+
+(* checked name *)
+
+fun checked_name check =
+  let fun intern tok = check (Token.content_of tok, Token.pos_of tok);
+  in internal_name >> #1 || Parse.token Parse.xname >> evaluate Token.name0 intern end;
+
 end;

--- a/src/Pure/Isar/method.ML	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 10 13:55:10 2015 +0100
@@ -75,8 +75,8 @@
   val position: text_range option -> Position.T
   val reports_of: text_range -> Position.report list
   val report: text_range -> unit
-  val parse0: text_range parser
   val parse: text_range parser
+  val parse_internal: Proof.context -> text_range parser
 end;
 
 structure Method: METHOD =
@@ -554,45 +554,58 @@
 end;
 
 
-(* outer parser *)
+(* parser *)
+
+local
 
 fun is_symid_meth s =
   s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
 
-local
+fun parser check_ctxt low_pri =
+  let
+    val (meth_name, mk_src) =
+      (case check_ctxt of
+        NONE => (Parse.xname, Token.src)
+      | SOME ctxt =>
+         (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
+          fn name => fn args => #1 (check_src ctxt (Token.src name args))));
 
-fun meth5 x =
- (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
-  Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
-    Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
-  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
-and meth4 x =
- (meth5 -- Parse.position (Parse.$$$ "?")
-    >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
-  meth5 -- Parse.position (Parse.$$$ "+")
-    >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
-  meth5 --
-    (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
-    >> (fn (m, (((_, pos1), n), (_, pos2))) =>
-        Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
-  meth5) x
-and meth3 x =
- (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
-  meth4) x
-and meth2 x =
-  (Parse.enum1_positions "," meth3
-    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
-and meth1 x =
-  (Parse.enum1_positions ";" meth2
-    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x
-and meth0 x =
-  (Parse.enum1_positions "|" meth1
-    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
+    fun meth5 x =
+     (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||
+      Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
+        Source (mk_src ("cartouche", Token.pos_of tok) [tok])) ||
+      Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
+    and meth4 x =
+     (meth5 -- Parse.position (Parse.$$$ "?")
+        >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
+      meth5 -- Parse.position (Parse.$$$ "+")
+        >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
+      meth5 --
+        (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
+        >> (fn (m, (((_, pos1), n), (_, pos2))) =>
+            Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
+      meth5) x
+    and meth3 x =
+     (Parse.position meth_name -- Parse.args1 is_symid_meth >> (Source o uncurry mk_src) ||
+      meth4) x
+    and meth2 x =
+      (Parse.enum1_positions "," meth3
+        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
+    and meth1 x =
+      (Parse.enum1_positions ";" meth2
+        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x
+    and meth0 x =
+      (Parse.enum1_positions "|" meth1
+        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
+  in
+    Scan.trace (if low_pri then meth0 else meth4)
+      >> (fn (m, toks) => (m, Token.range_of toks))
+  end;
 
 in
 
-val parse0 = Scan.trace meth0 >> (fn (m, toks) => (m, Token.range_of toks));
-val parse = Scan.trace meth4 >> (fn (m, toks) => (m, Token.range_of toks));
+val parse = parser NONE false;
+fun parse_internal ctxt = parser (SOME ctxt) true;
 
 end;
 

--- a/src/Pure/Isar/token.ML	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/Pure/Isar/token.ML	Tue Mar 10 13:55:10 2015 +0100
@@ -206,13 +206,15 @@
   if null args then pos
   else Position.set_range (pos, #2 (range_of args));
 
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
-  let
-    val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
-    val space = Name_Space.space_of_table table;
-    val kind = Name_Space.kind_of space;
-    val markup = Name_Space.markup space name;
-  in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
+fun check_src _ table (src as Src {name = (name, _), output_info = SOME _, ...}) =
+      (src, Name_Space.get table name)
+  | check_src ctxt table (Src {name = (xname, pos), args, output_info = NONE}) =
+      let
+        val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
+        val space = Name_Space.space_of_table table;
+        val kind = Name_Space.kind_of space;
+        val markup = Name_Space.markup space name;
+      in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
 
 
 (* stopper *)