# HG changeset patch
# User wenzelm
# Date 1303577161 -7200
# Node ID daa93275880eb5f6bb7b8688c55037fe4ba7c5ca
# Parent  aea61c5f88c33edc54761b434705ef260d28b90a
clarified Consts.read_const;

diff -r aea61c5f88c3 -r daa93275880e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:25:50 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:46:01 2011 +0200
@@ -462,7 +462,7 @@
       (case Variable.lookup_const ctxt c of
         SOME d =>
           Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
-      | NONE => Consts.read_const consts c);
+      | NONE => Consts.read_const consts (c, pos));
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
diff -r aea61c5f88c3 -r daa93275880e src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Apr 23 18:25:50 2011 +0200
+++ b/src/Pure/consts.ML	Sat Apr 23 18:46:01 2011 +0200
@@ -25,7 +25,7 @@
   val extern: Proof.context -> T -> string -> xstring
   val intern_syntax: T -> xstring -> string
   val extern_syntax: Proof.context -> T -> string -> xstring
-  val read_const: T -> string -> term
+  val read_const: T -> string * Position.T -> term
   val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
@@ -144,10 +144,10 @@
 
 (* read_const *)
 
-fun read_const consts raw_c =
+fun read_const consts (raw_c, pos) =
   let
     val c = intern consts raw_c;
-    val T = type_scheme consts c handle TYPE (msg, _, _) => error msg;
+    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
   in Const (c, T) end;