--- a/Quotient-Paper/Paper.thy	Mon Jul 19 07:49:10 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Mon Jul 19 08:34:38 2010 +0100
@@ -856,12 +856,12 @@
   on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
   which can all be performed independently from each other.
 
-  We first define the function @{text REG}, which takes terms of the 
+  We first define the function @{text REG}, which takes the terms of the 
   @{text "raw_thm"} and @{text "quot_thm"} as input and returns
-  @{text "reg_thm"}. The intuition
+  @{text "reg_thm"}. The idea
   behind this function is that it replaces quantifiers and
   abstractions involving raw types by bounded ones, and equalities
-  involving raw types are replaced by appropriate aggregate
+  involving raw types by appropriate aggregate
   equivalence relations. It is defined by simultaneously recursing on 
   the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
 
@@ -993,7 +993,7 @@
   the lambda preservation theorem. Given
   @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 
-    @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+  @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
 
   \noindent
   Next, relations over lifted types are folded to equalities.