Quot/QuotOption.thy
changeset 779 3b21b24a5fb6
parent 698 ed44eaaea63e
child 829 42b90994ac77
--- a/Quot/QuotOption.thy	Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/QuotOption.thy	Wed Dec 23 10:31:54 2009 +0100
@@ -16,7 +16,8 @@
   "option_map f None = None"
 | "option_map f (Some x) = Some (f x)"
 
-declare [[map * = (option_map, option_rel)]]
+declare [[map option = (option_map, option_rel)]]
+
 
 lemma option_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"