src/HOL/Library/Saturated.thy

--- a/src/HOL/Library/Saturated.thy	Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 24 13:33:42 2015 +0200
@@ -12,7 +12,7 @@
 
 subsection \<open>The type of saturated naturals\<close>
 
-typedef ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
   morphisms nat_of Abs_sat
   by auto