src/HOL/Typerep.thy
changeset 45693 bbd2c7ffc02c
parent 43329 84472e198515
child 48272 db75b4005d9a
     1.1 --- a/src/HOL/Typerep.thy	Wed Nov 30 16:03:18 2011 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Wed Nov 30 16:05:15 2011 +0100
     1.3 @@ -63,8 +63,9 @@
     1.4      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
     1.5    end;
     1.6  
     1.7 -fun ensure_typerep tyco thy = 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 +fun ensure_typerep tyco thy =
    1.10 +  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
    1.11 +    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
    1.12    then add_typerep tyco thy else thy;
    1.13  
    1.14  in