src/HOL/Typerep.thy
changeset 48272 db75b4005d9a
parent 45693 bbd2c7ffc02c
child 51112 da97167e03f7
     1.1 --- a/src/HOL/Typerep.thy	Mon Jul 16 15:57:21 2012 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Mon Jul 16 21:20:56 2012 +0200
     1.3 @@ -64,8 +64,8 @@
     1.4    end;
     1.5  
     1.6  fun ensure_typerep tyco thy =
     1.7 -  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
     1.8 -    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
     1.9 +  if not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep})
    1.10 +    andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort type}
    1.11    then add_typerep tyco thy else thy;
    1.12  
    1.13  in