# HG changeset patch
# User wenzelm
# Date 1135207733 -3600
# Node ID bb7b309ac395cdad6902390cd9d83e0fb4f1c42b
# Parent  389a6f9c31f49243525a5701549e249f17845462
Tactic.precise_conjunction_tac;

diff -r 389a6f9c31f4 -r bb7b309ac395 src/Pure/axclass.ML
--- 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