# HG changeset patch
# User wenzelm
# Date 974829843 -3600
# Node ID ea5de7c64c23318a1d1fe0b842b2d5aeb3ff5967
# Parent  01333dbe1431bc05169853d880d56f15af1dce3f
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;

diff -r 01333dbe1431 -r ea5de7c64c23 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Nov 21 19:03:27 2000 +0100
+++ b/src/Pure/axclass.ML	Tue Nov 21 19:04:03 2000 +0100
@@ -308,8 +308,9 @@
 (* intro_classes *)
 
 fun intro_classes_tac facts i st =
-  (Method.insert_tac facts THEN'
-    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i st;
+  ((Method.insert_tac facts THEN'
+    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i
+    THEN Tactic.distinct_subgoals_tac) st;    (*affects all subgoals!?*)
 
 val intro_classes_method =
   ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
@@ -318,8 +319,7 @@
 
 (* default method *)
 
-fun default_intro_classes_tac [] i = intro_classes_tac [] i THEN
-      Tactic.distinct_subgoals_tac    (*affects all subgoals, which is usually OK*)
+fun default_intro_classes_tac [] i = intro_classes_tac [] i
   | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
 
 fun default_tac rules ctxt facts =