more decisive commitment to get_free vs. the_const;
tuned;

--- a/src/Pure/General/position.ML	Thu Mar 06 16:33:48 2014 +0100
+++ b/src/Pure/General/position.ML	Thu Mar 06 17:37:32 2014 +0100
@@ -43,6 +43,7 @@
   val reports: report list -> unit
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
+  val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
@@ -182,6 +183,9 @@
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
+fun append_reports (r: report_text list Unsynchronized.ref) reports =
+  Unsynchronized.change r (append (map (rpair "") reports));
+
 
 (* here: inlined formal markup *)
 

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 16:33:48 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 17:37:32 2014 +0100
@@ -73,7 +73,7 @@
   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
+    xstring * Position.T list -> term * Position.report list
   val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
@@ -476,31 +476,31 @@
   |> implode
   |> Markup.markup_report;
 
-fun check_const ctxt {proper, strict} (c, pos) =
+fun check_const ctxt {proper, strict} (c, ps) =
   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);
+      Name.reject_internal (c, ps) handle ERROR msg =>
+        error (msg ^ consts_completion_message ctxt (c, ps));
+    fun err msg = error (msg ^ Position.here_list ps);
     val consts = consts_of ctxt;
     val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
     val (t, reports) =
       (case (fixed, Variable.lookup_const ctxt c) of
         (SOME x, NONE) =>
           let
-            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))]
-              else [];
+            val reports = ps
+              |> filter (Context_Position.is_reported ctxt)
+              |> map (fn pos =>
+                (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
           in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       | (_, SOME d) =>
           let
             val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
-            val reports =
-              if Context_Position.is_reported ctxt pos
-              then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
+            val reports = ps
+              |> filter (Context_Position.is_reported ctxt)
+              |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
           in (Const (d, T), reports) end
-      | _ => Consts.check_const (Context.Proof ctxt) consts (c, [pos]));
+      | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>
@@ -510,8 +510,8 @@
 
 fun read_const ctxt flags text =
   let
-    val (t, reports) =
-      check_const ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val (t, reports) = check_const ctxt flags (xname, [pos]);
     val _ = Position.reports reports;
   in t end;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:33:48 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 17:37:32 2014 +0100
@@ -140,6 +140,7 @@
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report pos = Position.store_reports reports [pos];
+    val append_reports = Position.append_reports reports;
 
     fun trans a args =
       (case trf a of
@@ -164,7 +165,7 @@
           let
             val pos = Lexicon.pos_of_token tok;
             val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
-            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+            val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
@@ -172,7 +173,7 @@
             val (Type (c, _), rs) =
               Proof_Context.check_type_name ctxt {proper = true, strict = false}
                 (Lexicon.str_of_token tok, pos);
-            val _ = Unsynchronized.change reports (append (map (rpair "") rs));
+            val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
@@ -221,22 +222,23 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun decode_const ctxt c =
+fun decode_const ctxt (c, ps) =
   let
-    val (Const (c', _), _) =
-      Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none);
-  in c' end;
+    val (Const (c', _), reports) =
+      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
+  in (c', reports) end;
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
-        fun get_const c =
-          (true, decode_const ctxt c) handle ERROR _ =>
-            (false, Consts.intern (Proof_Context.consts_of ctxt) c);
+        val reports = Unsynchronized.ref reports0;
+        fun report ps = Position.store_reports reports ps;
+        val append_reports = Position.append_reports reports;
+
         fun get_free x =
           let
             val fixed = Variable.lookup_fixed ctxt x;
-            val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x;
+            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
             val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
           in
             if Variable.is_const ctxt x then NONE
@@ -245,8 +247,11 @@
             else NONE
           end;
 
-        val reports = Unsynchronized.ref reports0;
-        fun report ps = Position.store_reports reports ps;
+        fun the_const (a, ps) =
+          let
+            val (c, rs) = decode_const ctxt (a, ps);
+            val _ = append_reports rs;
+          in c end;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
@@ -269,20 +274,15 @@
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
-                        SOME c => c
-                      | NONE => snd (get_const a));
-                    val _ = report ps (markup_const ctxt) c;
+                        SOME c => (report ps (markup_const ctxt) c; c)
+                      | NONE => the_const (a, ps));
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, 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))))
+                (case get_free a of
+                  SOME x => (report ps (markup_free ctxt) x; Free (x, T))
+                | NONE => Const (the_const (a, ps), 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
@@ -813,7 +813,7 @@
 
 fun const_ast_tr intern ctxt [Ast.Variable c] =
       let
-        val c' = decode_const ctxt c;
+        val (c', _) = decode_const ctxt (c, []);
         val d = if intern then Lexicon.mark_const c' else c;
       in Ast.Constant d end
   | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =