--- a/Nominal/FSet.thy	Mon Jun 14 13:24:22 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 14:44:18 2010 +0200
@@ -1662,5 +1662,10 @@
 apply(auto simp add: mem_def)
 done
 
+lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
+apply rule
+apply (rule ball_reg_right)
+apply auto
+done
 
 end

--- a/Quotient-Paper/Paper.thy	Mon Jun 14 13:24:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 14:44:18 2010 +0200
@@ -797,13 +797,13 @@
 
   Isabelle provides a set of \emph{mono} rules, that are used to split implications
   of similar statements into simpler implication subgoals. These are enhanced
-  with special quotient theorem in the regularization goal. Below we only show
+  with special quotient theorem in the regularization proof. Below we only show
   the versions for the universal quantifier. For the existential quantifier
   and abstraction they are analogous.
 
   First, bounded universal quantifiers can be removed on the right:
 
-  @{thm [display, indent=10] ball_reg_right[no_vars]}
+  @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}
 
   They can be removed anywhere if the relation is an equivalence relation: