clarified treatment of consts -- prefer value-oriented reports;

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:53:14 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 11:32:16 2014 +0100
@@ -74,6 +74,8 @@
     xstring * Position.T -> typ * Position.report list
   val read_type_name: Proof.context -> bool -> string -> typ
   val read_type_name_proper: Proof.context -> bool -> string -> typ
+  val check_const_proper: Proof.context -> bool ->
+    xstring * Position.T -> term * Position.report list
   val read_const_proper: Proof.context -> bool -> string -> term
   val read_const: Proof.context -> bool -> typ -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
@@ -82,7 +84,6 @@
   val prepare_sortsT: Proof.context -> typ list -> string * typ list
   val prepare_sorts: Proof.context -> term list -> string * term list
   val check_tfree: Proof.context -> string * sort -> string * sort
-  val intern_skolem: Proof.context -> string -> string option
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
@@ -474,45 +475,49 @@
 
 (* constant names *)
 
-local
-
-fun prep_const_proper ctxt strict (c, pos) =
+fun check_const_proper ctxt strict (c, pos) =
   let
     fun err msg = error (msg ^ Position.here pos);
     val consts = consts_of ctxt;
-    val t as Const (d, _) =
+    val (t as Const (d, _), reports) =
       (case Variable.lookup_const ctxt c of
         SOME d =>
           let
             val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
-            val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
-          in Const (d, T) end
+            val reports =
+              if Context_Position.is_reported ctxt pos
+              then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
+          in (Const (d, T), reports) end
       | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
     val _ =
       if strict
       then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
       else ();
-  in t end;
+  in (t, reports) end;
 
-in
-
-fun read_const_proper ctxt strict =
-  prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
+fun read_const_proper ctxt strict text =
+  let
+    val (t, reports) =
+      check_const_proper ctxt strict (Symbol_Pos.source_content (Syntax.read_token text));
+    val _ = Position.reports reports;
+  in t end;
 
 fun read_const ctxt strict ty text =
   let
     val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
     val _ = Name.reject_internal (c, [pos]);
-  in
-    (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
-      (SOME x, false) =>
-        (Context_Position.report ctxt pos
-            (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free));
-          Free (x, infer_type ctxt (x, ty)))
-    | _ => prep_const_proper ctxt strict (c, pos))
-  end;
-
-end;
+    val (t, reports) =
+      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
+        (SOME x, false) =>
+          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 [];
+          in (Free (x, infer_type ctxt (x, ty)), reports) end
+      | _ => check_const_proper ctxt strict (c, pos));
+    val _ = Position.reports reports;
+  in t end;
 
 
 (* type arities *)
@@ -533,21 +538,6 @@
 end;
 
 
-(* skolem variables *)
-
-fun intern_skolem ctxt x =
-  let
-    val skolem = Variable.lookup_fixed ctxt x;
-    val is_const = can (read_const_proper ctxt false) 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
-    else if is_some skolem then skolem
-    else if not is_const orelse is_declared then SOME x
-    else NONE
-  end;
-
-
 (* read_term *)
 
 fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:53:14 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 11:32:16 2014 +0100
@@ -220,13 +220,27 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
+fun decode_const ctxt c =
+  let val (Const (c', _), _) = Proof_Context.check_const_proper ctxt false (c, Position.none)
+  in c' end;
+
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
-        fun get_const a =
-          ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
-            handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
-        val get_free = Proof_Context.intern_skolem ctxt;
+        fun get_const c =
+          (true, decode_const ctxt c) handle ERROR _ =>
+            (false, Consts.intern (Proof_Context.consts_of ctxt) c);
+        fun get_free x =
+          let
+            val skolem = Variable.lookup_fixed ctxt 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
+            else if is_some skolem then skolem
+            else if not is_const orelse is_declared then SOME x
+            else NONE
+          end;
 
         val reports = Unsynchronized.ref reports0;
         fun report ps = Position.store_reports reports ps;
@@ -796,7 +810,7 @@
 
 fun const_ast_tr intern ctxt [Ast.Variable c] =
       let
-        val Const (c', _) = Proof_Context.read_const_proper ctxt false 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]] =

--- a/src/Pure/consts.ML	Thu Mar 06 10:53:14 2014 +0100
+++ b/src/Pure/consts.ML	Thu Mar 06 11:32:16 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
+  val check_const: Context.generic -> T -> xstring * Position.T -> 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
@@ -146,9 +146,9 @@
 fun check_const context consts (xname, pos) =
   let
     val Consts {decls, ...} = consts;
-    val (c, _) = Name_Space.check context decls (xname, pos);
+    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);
-  in Const (c, T) end;
+  in (Const (c, T), reports) end;
 
 
 (* certify *)