diff -r 4bba0d41ff2c -r 8954dc5ebd52 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Jun 14 14:28:12 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 14:28:32 2010 +0200
@@ -1672,5 +1672,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