default_intro_classes_tac: Tactic.distinct_subgoals_tac;
authorwenzelm
Sat Nov 18 19:47:36 2000 +0100 (2000-11-18 ago)
changeset 1049376e05ec87b57
parent 10492 107c7db021a9
child 10494 305b37c8d8a3
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Sat Nov 18 19:47:12 2000 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sat Nov 18 19:47:36 2000 +0100
     1.3 @@ -318,8 +318,9 @@
     1.4  
     1.5  (* default method *)
     1.6  
     1.7 -fun default_intro_classes_tac [] = intro_classes_tac []
     1.8 -  | default_intro_classes_tac _ = K Tactical.no_tac;    (*no error message!*)
     1.9 +fun default_intro_classes_tac [] i = intro_classes_tac [] i THEN
    1.10 +      Tactic.distinct_subgoals_tac    (*affects all subgoals, which is usually OK*)
    1.11 +  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
    1.12  
    1.13  fun default_tac rules ctxt facts =
    1.14    HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);