reject internal term names outright, and complete consts instead;
more general Name_Space.check_reports;
more compact Markup.markup_report;

--- a/src/Pure/General/name_space.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -56,7 +56,7 @@
   val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table
   val check_reports: Context.generic -> 'a table ->
-    xstring * Position.T -> (string * Position.report list) * 'a
+    xstring * Position.T list -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -446,24 +446,27 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun check_reports context (space, tab) (xname, pos) =
+fun check_reports context (space, tab) (xname, ps) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
       SOME x =>
         let
           val reports =
-            if Context_Position.is_reported_generic context pos
-            then [(pos, markup space name)] else [];
+            filter (Context_Position.is_reported_generic context) ps
+            |> map (fn pos => (pos, markup space name));
         in ((name, reports), x) end
     | NONE =>
-        error (undefined (kind_of space) name ^ Position.here pos ^
-          Markup.markup Markup.report
-            (Completion.reported_text (completion context space (xname, pos)))))
+        let
+          val completions = map (fn pos => completion context space (xname, pos)) ps;
+        in
+          error (undefined (kind_of space) name ^ Position.here_list ps ^
+            implode (map (Markup.markup_report o Completion.reported_text) completions))
+        end)
   end;
 
-fun check context table arg =
+fun check context table (xname, pos) =
   let
-    val ((name, reports), x) = check_reports context table arg;
+    val ((name, reports), x) = check_reports context table (xname, [pos]);
     val _ = Position.reports reports;
   in (name, x) end;
 

--- a/src/Pure/Isar/args.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -299,7 +299,7 @@
     | (_, (_, args2)) =>
         error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
           (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
-          Markup.markup Markup.report (reported_text ())))
+          Markup.markup_report (reported_text ())))
   end;
 
 fun context_syntax kind scan src =

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -71,6 +71,7 @@
   val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     xstring * Position.T -> typ * Position.report list
   val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
+  val consts_completion_message: Proof.context -> xstring * Position.T list -> string
   val check_const: Proof.context -> {proper: bool, strict: bool} ->
     xstring * Position.T -> term * Position.report list
   val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
@@ -384,9 +385,8 @@
     val name = Type.cert_class tsig (Type.intern_class tsig xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
-          Markup.markup Markup.report
-            (Completion.reported_text
-              (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
+          Markup.markup_report (Completion.reported_text
+            (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
@@ -469,8 +469,18 @@
 
 (* constant names *)
 
+fun consts_completion_message ctxt (c, ps) =
+  ps |> map (fn pos =>
+    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+    |> Completion.reported_text)
+  |> implode
+  |> Markup.markup_report;
+
 fun check_const ctxt {proper, strict} (c, pos) =
   let
+    val _ =
+      Name.reject_internal (c, [pos]) handle ERROR msg =>
+        error (msg ^ consts_completion_message ctxt (c, [pos]));
     fun err msg = error (msg ^ Position.here pos);
     val consts = consts_of ctxt;
     val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
@@ -478,7 +488,6 @@
       (case (fixed, Variable.lookup_const ctxt c) of
         (SOME x, NONE) =>
           let
-            val _ = Name.reject_internal (c, [pos]);
             val reports =
               if Context_Position.is_reported ctxt pos then
                 [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
@@ -491,7 +500,7 @@
               if Context_Position.is_reported ctxt pos
               then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
           in (Const (d, T), reports) end
-      | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
+      | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos]));
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>

--- a/src/Pure/PIDE/markup.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -189,6 +189,7 @@
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markup_only: T -> string
+  val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
@@ -602,4 +603,7 @@
 
 fun markup_only m = markup m "";
 
+fun markup_report "" = ""
+  | markup_report txt = markup report txt;
+
 end;

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -274,14 +274,15 @@
                     val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
-              (Name.reject_internal (a, ps);
-               case (get_free a, get_const a) of
-                (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
-              | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
-              | (_, (false, c)) =>
-                  if Long_Name.is_qualified c
-                  then (report ps (markup_const ctxt) c; Const (c, T))
-                  else (report ps (markup_free ctxt) c; Free (c, T)))
+              ((Name.reject_internal (a, ps) handle ERROR msg =>
+                  error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
+                (case (get_free a, get_const a) of
+                  (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
+                | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
+                | (_, (false, c)) =>
+                    if Long_Name.is_qualified c
+                    then (report ps (markup_const ctxt) c; Const (c, T))
+                    else (report ps (markup_free ctxt) c; Free (c, T))))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
@@ -322,8 +323,7 @@
 
     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
-        error (msg ^
-          implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+        error (msg ^ implode (map (Markup.markup_report o Lexicon.reported_token_range ctxt) toks));
     val len = length pts;
 
     val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -355,7 +355,7 @@
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
-    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
+    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
   Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort

--- a/src/Pure/consts.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/consts.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -25,7 +25,7 @@
   val extern: Proof.context -> T -> string -> xstring
   val intern_syntax: T -> xstring -> string
   val extern_syntax: Proof.context -> T -> string -> xstring
-  val check_const: Context.generic -> T -> xstring * Position.T -> term * Position.report list
+  val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
   val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
@@ -143,11 +143,11 @@
 
 (* check_const *)
 
-fun check_const context consts (xname, pos) =
+fun check_const context consts (xname, ps) =
   let
     val Consts {decls, ...} = consts;
-    val ((c, reports), _) = Name_Space.check_reports context decls (xname, pos);
-    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
+    val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
+    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
   in (Const (c, T), reports) end;
 
 

--- a/src/Pure/type.ML	Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/type.ML	Thu Mar 06 16:12:26 2014 +0100
@@ -259,7 +259,8 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
+fun check_decl context (TSig {types, ...}) (c, pos) =
+  Name_Space.check_reports context types (c, [pos]);
 
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of