--- a/Quot/QuotMain.thy	Wed Feb 10 10:55:14 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Feb 10 11:09:30 2010 +0100
@@ -140,7 +140,7 @@
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
-  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True  (P x))"
+  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
 by (simp_all add: Quot_True_def ext)
 
@@ -169,7 +169,7 @@
   {* Sets up the three goals for the lifting procedure. *}
 
 method_setup regularize =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac)  *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
   {* Proves automatically the regularization goals from the lifting procedure. *}
 
 method_setup injection =