diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Mon Jul 16 15:57:21 2012 +0200 +++ b/src/HOL/Typerep.thy Mon Jul 16 21:20:56 2012 +0200 @@ -64,8 +64,8 @@ end; fun ensure_typerep tyco thy = - if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}) - andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type} + if not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}) + andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort type} then add_typerep tyco thy else thy; in