--- a/src/Pure/axclass.ML Thu Dec 22 00:28:52 2005 +0100
+++ b/src/Pure/axclass.ML Thu Dec 22 00:28:53 2005 +0100
@@ -283,8 +283,9 @@
val _ = message ("Proving type arity " ^ txt ^ " ...");
val props = (mk_arities arity);
val ths = Goal.prove_multi thy [] [] props
- (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) handle ERROR_MESSAGE msg =>
- error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
+ (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac)
+ handle ERROR_MESSAGE msg =>
+ error (msg ^ "\nThe error(s) above occurred while trying to prove " ^ txt);
in add_arity_thms ths thy end;
in