diff -r 2a95188263ec -r 9c44db3eef95 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 07:54:30 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 07:58:33 2010 +0200
@@ -874,7 +874,7 @@
 
   They can be removed anywhere if the relation is an equivalence relation:
 
-  @{thm [display, indent=10] ball_reg_eqv[no_vars]}
+  @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
 
   And finally it can be removed anywhere if @{term R2} is an equivalence relation: