changeset 16894 | 40f80823b451 |
parent 16723 | 9a9c034f1d57 |
child 16941 | 0bda949449ee |
--- a/src/Pure/sign.ML Tue Jul 19 20:47:00 2005 +0200 +++ b/src/Pure/sign.ML Tue Jul 19 20:47:01 2005 +0200 @@ -260,9 +260,7 @@ (case const_type thy c of SOME T => T | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); -fun declared_tyname thy c = - is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c)); - +val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of; val declared_const = is_some oo const_type;