equal
deleted
inserted
replaced
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, [], [])); |