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