src/Pure/sign.ML
changeset 17037 bd15f69bd947
parent 16988 02cd0c8b96d9
child 17039 78159411623f
equal deleted inserted replaced
17036:9b57e5aa4c93 17037:bd15f69bd947
    96   val typ_instance: theory -> typ * typ -> bool
    96   val typ_instance: theory -> typ * typ -> bool
    97   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    97   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    98   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    98   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    99   val is_logtype: theory -> string -> bool
    99   val is_logtype: theory -> string -> bool
   100   val const_constraint: theory -> string -> typ option
   100   val const_constraint: theory -> string -> typ option
       
   101   val the_const_constraint: theory -> string -> typ
   101   val const_type: theory -> string -> typ option
   102   val const_type: theory -> string -> typ option
   102   val the_const_type: theory -> string -> typ
   103   val the_const_type: theory -> string -> typ
   103   val declared_tyname: theory -> string -> bool
   104   val declared_tyname: theory -> string -> bool
   104   val declared_const: theory -> string -> bool
   105   val declared_const: theory -> string -> bool
   105   val class_space: theory -> NameSpace.T
   106   val class_space: theory -> NameSpace.T
   274     (case Symtab.lookup (constraints, c) of
   275     (case Symtab.lookup (constraints, c) of
   275       NONE => Option.map #1 (Symtab.lookup (consts, c))
   276       NONE => Option.map #1 (Symtab.lookup (consts, c))
   276     | some => some)
   277     | some => some)
   277   end;
   278   end;
   278 
   279 
       
   280 fun the_const_constraint thy c =
       
   281   (case const_constraint thy c of SOME T => T
       
   282   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
       
   283 
   279 fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
   284 fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
   280 
   285 
   281 fun the_const_type thy c =
   286 fun the_const_type thy c =
   282   (case const_type thy c of SOME T => T
   287   (case const_type thy c of SOME T => T
   283   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   288   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));