# 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