src/HOL/Set.thy

--- a/src/HOL/Set.thy	Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Set.thy	Mon Jul 06 21:24:30 2009 +0200
@@ -449,7 +449,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}) *}
+ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
 
 text {*
   \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and