--- a/src/Pure/consts.ML Thu Mar 06 14:38:54 2014 +0100
+++ b/src/Pure/consts.ML Thu Mar 06 16:12:26 2014 +0100
@@ -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 check_const: Context.generic -> T -> xstring * Position.T -> term * Position.report list
+ val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
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
@@ -143,11 +143,11 @@
(* check_const *)
-fun check_const context consts (xname, pos) =
+fun check_const context consts (xname, ps) =
let
val Consts {decls, ...} = consts;
- val ((c, reports), _) = Name_Space.check_reports context decls (xname, pos);
- val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
+ val ((c, reports), _) = Name_Space.check_reports context decls (xname, ps);
+ val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here_list ps);
in (Const (c, T), reports) end;