--- a/Quotient-Paper/Paper.thy	Thu Aug 19 15:02:11 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Thu Aug 19 15:46:28 2010 +0900
@@ -720,9 +720,9 @@
   theorems}. However, unlike his quotient package, we might have several
   respectfulness theorems for one constant---he has at most one.
   The reason is that because of our quotient compositions, the types
-  @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}.
-  And for every instantiation of the types, we might end up with a 
-  corresponding respectfulness theorem.
+  @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
+  And for every instantiation of the types, a corresponding
+  respectfulness theorem is necessary.
 
   Before lifting a theorem, we require the user to discharge
   respectfulness proof obligations. In case of @{text bn}