# HG changeset patch
# User wenzelm
# Date 1349277128 -7200
# Node ID 74ad6ecf2af21705d20eaeb7ca959d019b2dfc4c
# Parent  a6814de45b69be668cdb7f00e11f89794f5f484d
more error positions;

diff -r a6814de45b69 -r 74ad6ecf2af2 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Oct 03 16:59:58 2012 +0200
+++ b/src/Pure/General/position.ML	Wed Oct 03 17:12:08 2012 +0200
@@ -42,6 +42,7 @@
   val reports: report list -> unit
   val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val here: T -> string
+  val here_list: T list -> string
   type range = T * T
   val no_range: range
   val set_range: range -> T
@@ -198,6 +199,8 @@
         Markup.markup (Markup.properties props Isabelle_Markup.position) s
   end;
 
+val here_list = space_implode " " o map here;
+
 
 (* range *)
 
diff -r a6814de45b69 -r 74ad6ecf2af2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Oct 03 16:59:58 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Oct 03 17:12:08 2012 +0200
@@ -630,8 +630,7 @@
           Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
             handle Vartab.DUP _ =>
               error ("Inconsistent sort constraints for type variable " ^
-                quote (Term.string_of_vname' xi) ^
-                space_implode " " (map Position.here ps))
+                quote (Term.string_of_vname' xi) ^ Position.here_list ps)
       end;
 
     val env =
@@ -658,7 +657,11 @@
           :: reports
       else reports;
 
-    val decode_pos = #1 o Term_Position.decode_positionS;
+    fun get_sort_reports xi raw_S =
+      let
+        val ps = #1 (Term_Position.decode_positionS raw_S);
+        val S = get_sort xi handle ERROR msg => error (msg ^ Position.here_list ps);
+      in fold (add_report S) ps end;
 
     val reports =
       (fold o fold_atyps)
@@ -666,8 +669,8 @@
           if Term_Position.is_positionT T then I
           else
             (case T of
-              TFree (x, raw_S) => fold (add_report (get_sort (x, ~1))) (decode_pos raw_S)
-            | TVar (xi, raw_S) => fold (add_report (get_sort xi)) (decode_pos raw_S)
+              TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S
+            | TVar (xi, raw_S) => get_sort_reports xi raw_S
             | _ => I)) tys [];
 
   in (implode (map #2 reports), get_sort) end;