changeset 48272 | db75b4005d9a |
parent 45693 | bbd2c7ffc02c |
child 51112 | da97167e03f7 |
--- 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