diff -r 9b57e5aa4c93 -r bd15f69bd947 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Aug 09 08:56:34 2005 +0200
+++ b/src/Pure/sign.ML	Tue Aug 09 10:03:30 2005 +0200
@@ -98,6 +98,7 @@
   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
   val is_logtype: theory -> string -> bool
   val const_constraint: theory -> string -> typ option
+  val the_const_constraint: theory -> string -> typ
   val const_type: theory -> string -> typ option
   val the_const_type: theory -> string -> typ
   val declared_tyname: theory -> string -> bool
@@ -276,6 +277,10 @@
     | some => some)
   end;
 
+fun the_const_constraint thy c =
+  (case const_constraint thy c of SOME T => T
+  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
+
 fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
 
 fun the_const_type thy c =