changeset 56026 | 893fe12639bc |
parent 56025 | d74fed45fa8b |
child 56056 | 4d46d53566e6 |
--- a/src/Pure/sign.ML Mon Mar 10 13:55:03 2014 +0100 +++ b/src/Pure/sign.ML Mon Mar 10 15:04:01 2014 +0100 @@ -192,7 +192,7 @@ fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts)); -val declared_tyname = is_some oo (Name_Space.lookup_key o #types o Type.rep_tsig o tsig_of); +fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none); val declared_const = can o the_const_constraint;