diff -r 5e5ca36692b3 -r 9caab698dbe4 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Apr 03 16:26:48 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient_Option.thy
+(*  Title:      HOL/Library/Quotient3_Option.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
@@ -55,36 +55,36 @@
   by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
 
 lemma option_quotient [quot_thm]:
-  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 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]
+  assumes "Quotient3 R Abs Rep"
+  shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
+  apply (rule Quotient3I)
+  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
+  using Quotient3_rel [OF assms]
   apply (simp add: option_rel_unfold split: option.split)
   done
 
-declare [[map option = (option_rel, option_quotient)]]
+declare [[mapQ3 option = (option_rel, option_quotient)]]
 
 lemma option_None_rsp [quot_respect]:
-  assumes q: "Quotient R Abs Rep"
+  assumes q: "Quotient3 R Abs Rep"
   shows "option_rel R None None"
   by simp
 
 lemma option_Some_rsp [quot_respect]:
-  assumes q: "Quotient R Abs Rep"
+  assumes q: "Quotient3 R Abs Rep"
   shows "(R ===> option_rel R) Some Some"
   by auto
 
 lemma option_None_prs [quot_preserve]:
-  assumes q: "Quotient R Abs Rep"
+  assumes q: "Quotient3 R Abs Rep"
   shows "Option.map Abs None = None"
   by simp
 
 lemma option_Some_prs [quot_preserve]:
-  assumes q: "Quotient R Abs Rep"
+  assumes q: "Quotient3 R Abs Rep"
   shows "(Rep ---> Option.map Abs) Some = Some"
   apply(simp add: fun_eq_iff)
-  apply(simp add: Quotient_abs_rep[OF q])
+  apply(simp add: Quotient3_abs_rep[OF q])
   done
 
 end