inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

--- a/src/Pure/Isar/proof_context.ML	Thu Sep 02 23:37:14 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Sep 02 23:45:37 2010 +0200
@@ -741,14 +741,14 @@
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
-      handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
+      handle ERROR msg => cat_error msg "Failed to parse sort";
   in Type.minimize_sort (tsig_of ctxt) S end;
 
 fun parse_typ ctxt text =
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
     val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
-      handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
+      handle ERROR msg => cat_error msg "Failed to parse type";
   in T end;
 
 fun parse_term T ctxt text =
@@ -756,7 +756,8 @@
     val {get_sort, map_const, map_free} = term_context ctxt;
 
     val (T', _) = Type_Infer.paramify_dummies T 0;
-    val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
+    val (markup, kind) =
+      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     val (syms, pos) = Syntax.parse_token ctxt markup text;
 
     fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
@@ -764,7 +765,7 @@
     val t =
       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
-      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
+      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
   in t end;