src/HOL/Set.ML

--- a/src/HOL/Set.ML	Tue Mar 26 17:15:54 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 27 18:45:17 1996 +0100
@@ -70,10 +70,10 @@
 qed "bexE";
 
 (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
-val prems = goal Set.thy
-    "(! x:A. True) = True";
+goal Set.thy "(! x:A. True) = True";
 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
 qed "ball_rew";
+Addsimps [ball_rew];
 
 (** Congruence rules **)