src/HOL/Set.ML
changeset 9769 a73540153a73
parent 9687 772ac061bd76
child 9892 be0389a64ce8
     1.1 --- a/src/HOL/Set.ML	Fri Sep 01 00:28:06 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Sep 01 00:28:27 2000 +0200
     1.3 @@ -785,7 +785,7 @@
     1.4  
     1.5  fun gen_rulify_prems x =
     1.6    Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
     1.7 -    rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
     1.8 +    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, ballI, impI])))))) x;
     1.9  
    1.10  in
    1.11