# HG changeset patch
# User wenzelm
# Date 967760907 -7200
# Node ID a73540153a7399ed36843a5d26e06d69db581122
# Parent  a589b1d75b7b3cb0049c37e156b2dfcf94e9b62e
fixed rulify_prems;

diff -r a589b1d75b7b -r a73540153a73 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Sep 01 00:28:06 2000 +0200
+++ b/src/HOL/Set.ML	Fri Sep 01 00:28:27 2000 +0200
@@ -785,7 +785,7 @@
 
 fun gen_rulify_prems x =
   Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
-    rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
+    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, ballI, impI])))))) x;
 
 in