diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Feb 22 22:18:38 2006 +0100
+++ b/src/Pure/tactic.ML	Wed Feb 22 22:18:39 2006 +0100
@@ -642,8 +642,7 @@
 (* meta-level conjunction *)
 
 val conj_tac = SUBGOAL (fn (goal, i) =>
-  if can Logic.dest_conjunction goal then
-    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
+  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
   else no_tac);
 
 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;