src/HOL/Quotient_Examples/Lift_Fun.thy

--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -51,7 +51,7 @@
 
 text {* Registration of the map function for 'a endofun. *}
 
-enriched_type map_endofun : map_endofun
+functor map_endofun : map_endofun
 proof -
   have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
   then show "map_endofun id id = id"