changeset 19125 | 59b26248547b |
parent 19056 | 6ac9dfe98e54 |
child 19185 | 9fb741abb008 |
--- 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;