src/Pure/sign.ML
changeset 17037 bd15f69bd947
parent 16988 02cd0c8b96d9
child 17039 78159411623f
     1.1 --- a/src/Pure/sign.ML	Tue Aug 09 08:56:34 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 09 10:03:30 2005 +0200
     1.3 @@ -98,6 +98,7 @@
     1.4    val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
     1.5    val is_logtype: theory -> string -> bool
     1.6    val const_constraint: theory -> string -> typ option
     1.7 +  val the_const_constraint: theory -> string -> typ
     1.8    val const_type: theory -> string -> typ option
     1.9    val the_const_type: theory -> string -> typ
    1.10    val declared_tyname: theory -> string -> bool
    1.11 @@ -276,6 +277,10 @@
    1.12      | some => some)
    1.13    end;
    1.14  
    1.15 +fun the_const_constraint thy c =
    1.16 +  (case const_constraint thy c of SOME T => T
    1.17 +  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
    1.18 +
    1.19  fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
    1.20  
    1.21  fun the_const_type thy c =