more reports and error positions;

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 17:02:12 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:09:27 2011 +0200
@@ -366,6 +366,7 @@
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
     val _ = Context_Position.report ctxt pos (Markup.tclass c);
+    val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   in c end;
 
 
@@ -466,6 +467,7 @@
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
     val _ = Context_Position.report ctxt pos (Markup.const d);
+    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
   in t end;
 
 in
@@ -481,14 +483,15 @@
     else
       let
         val d = intern_type ctxt c;
-        val decl = Type.the_decl tsig d;
-        val _ = Context_Position.report ctxt pos (Markup.tycon d);
-        fun err () = error ("Bad type name: " ^ quote d);
+        val decl = Type.the_decl tsig d handle ERROR msg => error (msg ^ Position.str_of pos);
+        fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of 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 (Markup.tycon d);
+        val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
       in Type (d, replicate args dummyT) end
   end;