# HG changeset patch
# User wenzelm
# Date 1393790547 -3600
# Node ID a232c0ff3c2038f61d2786ef82b8abbc39d83f23
# Parent  2982d233d798c348af37e31b5989f0b5f6992cdf
prefer Name_Space.check with its builtin reports (including completion);

diff -r 2982d233d798 -r a232c0ff3c20 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 20:34:11 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 21:02:27 2014 +0100
@@ -472,15 +472,13 @@
       TFree (c, default_sort ctxt (c, ~1)))
     else
       let
-        val d = intern_type ctxt c;
-        val decl = Type.the_decl tsig (d, pos);
+        val (d, decl) = Type.check_decl (Context.Proof ctxt) tsig (c, pos);
         fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
         val args =
           (case decl of
             Type.LogicalType n => n
           | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
           | Type.Nonterminal => if strict then err () else 0);
-        val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
       in Type (d, replicate args dummyT) end
   end;
 
diff -r 2982d233d798 -r a232c0ff3c20 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Mar 02 20:34:11 2014 +0100
+++ b/src/Pure/type.ML	Sun Mar 02 21:02:27 2014 +0100
@@ -52,6 +52,7 @@
   val intern_type: tsig -> xstring -> string
   val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
+  val check_decl: Context.generic -> tsig -> xstring * Position.T -> string * decl
   val the_decl: tsig -> string * Position.T -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
@@ -257,6 +258,8 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
+fun check_decl context (TSig {types, ...}) = Name_Space.check context types;
+
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of
     NONE => error (undecl_type c ^ Position.here pos)