--- 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