diff -r f4d2ff3cad09 -r 54f130df1136 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Jul 11 13:54:32 2003 +0200
+++ b/src/HOL/Set.thy	Fri Jul 11 14:11:56 2003 +0200
@@ -247,6 +247,7 @@
 
 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
   by (unfold Ball_def) blast
+ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *}
 
 text {*
   \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and