# HG changeset patch
# User wenzelm
# Date 974573256 -3600
# Node ID 76e05ec87b57bf56b1e4ce7306ecb02e6c7b7af6
# Parent  107c7db021a9201ab546678fc65538df5a50c967
default_intro_classes_tac: Tactic.distinct_subgoals_tac;

diff -r 107c7db021a9 -r 76e05ec87b57 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Nov 18 19:47:12 2000 +0100
+++ b/src/Pure/axclass.ML	Sat Nov 18 19:47:36 2000 +0100
@@ -318,8 +318,9 @@
 
 (* default method *)
 
-fun default_intro_classes_tac [] = intro_classes_tac []
-  | default_intro_classes_tac _ = K Tactical.no_tac;    (*no error message!*)
+fun default_intro_classes_tac [] i = intro_classes_tac [] i THEN
+      Tactic.distinct_subgoals_tac    (*affects all subgoals, which is usually OK*)
+  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
 
 fun default_tac rules ctxt facts =
   HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);