# HG changeset patch
# User wenzelm
# Date 1118005646 -7200
# Node ID df2b550a17f6e312fbebd58473b2a9d2ffd27a42
# Parent  7a03b4b4df67690f105b9ddd4fb3111b716bcab1
added the_const_type;

diff -r 7a03b4b4df67 -r df2b550a17f6 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Jun 05 23:07:25 2005 +0200
+++ b/src/Pure/sign.ML	Sun Jun 05 23:07:26 2005 +0200
@@ -39,7 +39,9 @@
   val is_draft: sg -> bool
   val is_stale: sg -> bool
   val syn_of: sg -> Syntax.syntax
+  val naming_of: sg -> NameSpace.naming
   val const_type: sg -> string -> typ option
+  val the_const_type: sg -> string -> typ          (*exception TYPE*)
   val declared_tyname: sg -> string -> bool
   val declared_const: sg -> string -> bool
   val classes: sg -> class list
@@ -52,7 +54,6 @@
   val classK: string
   val typeK: string
   val constK: string
-  val naming_of: sg -> NameSpace.naming
   val base_name: string -> bstring
   val full_name: sg -> bstring -> string
   val full_name_path: sg -> string -> bstring -> string
@@ -99,7 +100,7 @@
   val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   val read_tyname: sg -> string -> typ
-  val read_const: sg -> string -> term
+  val read_const: sg -> string -> term        (*exception TYPE*)
   val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> xterm list * typ -> term * (indexname * typ) list
@@ -237,10 +238,15 @@
 val str_of_sg = Pretty.str_of o pretty_sg;
 val pprint_sg = Pretty.pprint o pretty_sg;
 
+fun naming_of (Sg (_, {naming, ...})) = naming;
 val tsig_of = #tsig o rep_sg;
 fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
+
 fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
-fun naming_of (Sg (_, {naming, ...})) = naming;
+
+fun the_const_type sg c =
+  (case const_type sg c of SOME T => T
+  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
 
 fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
 fun declared_const sg c = is_some (const_type sg c);
@@ -759,10 +765,8 @@
   end;
 
 fun read_const sg raw_c =
-  let val c = intern_const sg raw_c in
-    if is_some (const_type sg c) then Const (c, dummyT)
-    else raise TYPE ("Undeclared constant: " ^ quote c, [], [])
-  end;
+  let val c = intern_const sg raw_c
+  in the_const_type sg c; Const (c, dummyT) end;