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)