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