diff -r 6deb216d726f -r e44d24620515 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Mar 28 22:01:04 2008 +0100
+++ b/src/Provers/classical.ML	Fri Mar 28 22:01:56 2008 +0100
@@ -1019,7 +1019,7 @@
 
 fun default_tac rules ctxt cs facts =
   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
-  Class.default_intro_classes_tac facts;
+  Class.default_intro_tac ctxt facts;
 
 in
   val rule = METHOD_CLASET' o rule_tac;