--- a/Quotient-Paper/Paper.thy	Tue Jun 15 06:35:57 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 06:50:33 2010 +0200
@@ -366,7 +366,7 @@
 
   \noindent
   Unfortunately, restrictions in HOL's type-system prevent us from stating
-  and proving a quotient type theorem, like \ref{funquot}, for compositions 
+  and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions 
   of relations. However, we can prove all instances where @{text R\<^isub>1} and 
   @{text "R\<^isub>2"} are built up by constituent equivalence relations.
 *}