--- a/Quot/QuotOption.thy	Mon Jan 25 20:47:20 2010 +0100
+++ b/Quot/QuotOption.thy	Tue Jan 26 00:18:48 2010 +0100
@@ -1,7 +1,12 @@
+(*  Title:      QuotOption.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+*)
 theory QuotOption
 imports QuotMain
 begin
 
+section {* Quotient infrastructure for option type *}
+
 fun
   option_rel
 where
@@ -10,19 +15,12 @@
 | "option_rel R None (Some x) = False"
 | "option_rel R (Some x) (Some y) = R x y"
 
-fun
-  option_map
-where
-  "option_map f None = None"
-| "option_map f (Some x) = Some (f x)"
-
-declare [[map option = (option_map, option_rel)]]
-
+declare [[map option = (Option.map, option_rel)]]
 
 lemma option_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"
-  shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"
-  apply(unfold Quotient_def)
+  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
+  unfolding Quotient_def
   apply(auto)
   apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
   apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
@@ -63,18 +61,18 @@
 
 lemma option_None_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
-  shows "option_map Abs None = None"
+  shows "Option.map Abs None = None"
   by simp
 
 lemma option_Some_prs[quot_respect]:
   assumes q: "Quotient R Abs Rep"
-  shows "(Rep ---> option_map Abs) Some = Some"
+  shows "(Rep ---> Option.map Abs) Some = Some"
   apply(simp add: expand_fun_eq)
   apply(simp add: Quotient_abs_rep[OF q])
   done
 
 lemma option_map_id[id_simps]: 
-  shows "option_map id \<equiv> id"
+  shows "Option.map id \<equiv> id"
   apply (rule eq_reflection)
   apply (auto simp add: expand_fun_eq)
   apply (case_tac x)