--- 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