--- a/src/Pure/axclass.ML Wed Dec 06 21:19:03 2006 +0100
+++ b/src/Pure/axclass.ML Thu Dec 07 00:42:04 2006 +0100
@@ -257,7 +257,7 @@
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
- (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
+ (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
quote (Sign.string_of_arity thy arity));
in