--- a/Quot/quotient_tacs.ML	Wed Dec 23 13:23:33 2009 +0100
+++ b/Quot/quotient_tacs.ML	Wed Dec 23 13:45:42 2009 +0100
@@ -294,7 +294,7 @@
 To prove that the regularised theorem implies the abs/rep injected, 
 we try:
 
- 1) theorems 'trans2' from the appropriate QUOT_TYPE
+ 1) theorems 'trans2' from the appropriate Quot_Type
  2) remove lambdas from both sides: lambda_rsp_tac
  3) remove Ball/Bex from the right hand side
  4) use user-supplied RSP theorems