diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotOption.thy
--- a/Quot/QuotOption.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotOption.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -62,7 +62,7 @@
   shows "Option.map Abs None = None"
   by simp
 
-lemma option_Some_prs[quot_respect]:
+lemma option_Some_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> Option.map Abs) Some = Some"
   apply(simp add: expand_fun_eq)