src/Pure/type.ML

--- a/src/Pure/type.ML	Wed Mar 05 17:36:40 2014 +0100
+++ b/src/Pure/type.ML	Wed Mar 05 18:26:35 2014 +0100
@@ -52,7 +52,8 @@
   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 check_decl: Context.generic -> tsig ->
+    xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
@@ -258,7 +259,7 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun check_decl context (TSig {types, ...}) = Name_Space.check context types;
+fun check_decl context (TSig {types, ...}) = Name_Space.check_reports context types;
 
 fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of