src/HOL/Option.thy

--- a/src/HOL/Option.thy	Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Option.thy	Tue Jan 11 14:12:37 2011 +0100
@@ -81,7 +81,7 @@
     "map f o sum_case g h = sum_case (map f o g) (map f o h)"
   by (rule ext) (simp split: sum.split)
 
-type_lifting map: Option.map proof -
+enriched_type map: Option.map proof -
   fix f g
   show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
   proof