# HG changeset patch
# User wenzelm
# Date 953403593 -3600
# Node ID b6dd80ea3af1773ae7b8e70fb40f4ecd706ce80b
# Parent  981f52707e5d8b3c14fe6c8afbf72bf8443c8ee3
intro_classes_tac: REPEAT_ALL_NEW;

diff -r 981f52707e5d -r b6dd80ea3af1 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Mar 18 19:18:48 2000 +0100
+++ b/src/Pure/axclass.ML	Sat Mar 18 19:19:53 2000 +0100
@@ -305,11 +305,12 @@
 
 (* intro_classes *)
 
-fun intro_classes_tac st =
-  TRY (REPEAT_FIRST (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
+fun intro_classes_tac facts st =
+  FINDGOAL (Method.insert_tac facts THEN'
+      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
 
 val intro_classes_method =
-  ("intro_classes", Method.no_args (Method.METHOD0 intro_classes_tac),
+  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
     "back-chain introduction rules of axiomatic type classes");
 
 
@@ -325,7 +326,7 @@
     val defs = filter is_def thms;
     val non_defs = filter_out is_def thms;
   in
-    intro_classes_tac THEN
+    intro_classes_tac [] THEN
     TRY (rewrite_goals_tac defs) THEN
     TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   end;