src/Pure/axclass.ML

--- a/src/Pure/axclass.ML	Wed Apr 05 21:02:19 2000 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 05 21:02:31 2000 +0200
@@ -306,7 +306,7 @@
 (* intro_classes *)
 
 fun intro_classes_tac facts st =
-  FINDGOAL (Method.insert_tac facts THEN'
+  HEADGOAL (Method.insert_tac facts THEN'
       REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
 
 val intro_classes_method =