diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -60,7 +60,7 @@
   assumes "Quotient R Abs Rep"
   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
   apply (rule QuotientI)
-  apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
+  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
   using Quotient_rel [OF assms]
   apply (simp add: option_rel_unfold split: option.split)
   done