src/Pure/sign.ML
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;