--- a/src/Pure/consts.ML Sun Mar 02 21:13:29 2014 +0100
+++ b/src/Pure/consts.ML Sun Mar 02 21:30:47 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 read_const: T -> string * Position.T -> term
+ val check_const: Context.generic -> T -> xstring * 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
@@ -141,11 +141,12 @@
| NONE => s);
-(* read_const *)
+(* check_const *)
-fun read_const consts (raw_c, pos) =
+fun check_const context consts (xname, pos) =
let
- val c = intern consts raw_c;
+ val Consts {decls, ...} = consts;
+ val (c, _) = Name_Space.check context decls (xname, pos);
val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
in Const (c, T) end;