# HG changeset patch
# User wenzelm
# Date 1303575950 -7200
# Node ID aea61c5f88c33edc54761b434705ef260d28b90a
# Parent  1f7e39bdf0f682b4747f9cddcd6293a2c5d47dba
clarified Type.the_decl;

diff -r 1f7e39bdf0f6 -r aea61c5f88c3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:09:27 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:25:50 2011 +0200
@@ -483,7 +483,7 @@
     else
       let
         val d = intern_type ctxt c;
-        val decl = Type.the_decl tsig d handle ERROR msg => error (msg ^ Position.str_of pos);
+        val decl = Type.the_decl tsig (d, pos);
         fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of pos);
         val args =
           (case decl of
diff -r 1f7e39bdf0f6 -r aea61c5f88c3 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Apr 23 18:09:27 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Apr 23 18:25:50 2011 +0200
@@ -121,7 +121,7 @@
   >> (fn (ctxt, (s, pos)) =>
     let
       val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
-      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) c;
+      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
       val res =
         (case try check (c, decl) of
           SOME res => res
diff -r 1f7e39bdf0f6 -r aea61c5f88c3 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Apr 23 18:09:27 2011 +0200
+++ b/src/Pure/type.ML	Sat Apr 23 18:25:50 2011 +0200
@@ -51,7 +51,7 @@
   val intern_type: tsig -> xstring -> string
   val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
-  val the_decl: tsig -> string -> decl
+  val the_decl: tsig -> string * Position.T -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
@@ -246,9 +246,9 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun the_decl tsig c =
+fun the_decl tsig (c, pos) =
   (case lookup_type tsig c of
-    NONE => error (undecl_type c)
+    NONE => error (undecl_type c ^ Position.str_of pos)
   | SOME decl => decl);
 
 
@@ -277,7 +277,7 @@
             val Ts' = map cert Ts;
             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
           in
-            (case the_decl tsig c of
+            (case the_decl tsig (c, Position.none) of
               LogicalType n => (nargs n; Type (c, Ts'))
             | Abbreviation (vs, U, syn) =>
                (nargs (length vs);