# HG changeset patch
# User wenzelm
# Date 1393792247 -3600
# Node ID 3fa61f39d1f2cc7c746b1dbe4c3203ce145d039b
# Parent  ea540323c4440cc79c205df526ea7d12a155397e
prefer Name_Space.check with its builtin reports (including completion);

diff -r ea540323c444 -r 3fa61f39d1f2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 21:13:29 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 21:30:47 2014 +0100
@@ -480,12 +480,15 @@
     val t as Const (d, _) =
       (case Variable.lookup_const ctxt c of
         SOME d =>
-          Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
-      | NONE => Consts.read_const consts (c, pos));
+          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
+      | 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
+      if strict
+      then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
       else ();
-    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
   in t end;
 
 in
diff -r ea540323c444 -r 3fa61f39d1f2 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Mar 02 21:13:29 2014 +0100
+++ b/src/Pure/consts.ML	Sun Mar 02 21:30:47 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 read_const: T -> string * Position.T -> term
+  val check_const: Context.generic -> T -> xstring * Position.T -> term
   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
@@ -141,11 +141,12 @@
   | NONE => s);
 
 
-(* read_const *)
+(* check_const *)
 
-fun read_const consts (raw_c, pos) =
+fun check_const context consts (xname, pos) =
   let
-    val c = intern consts raw_c;
+    val Consts {decls, ...} = consts;
+    val (c, _) = Name_Space.check context decls (xname, pos);
     val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   in Const (c, T) end;