src/Pure/tactic.ML
changeset 19125 59b26248547b
parent 19056 6ac9dfe98e54
child 19185 9fb741abb008
     1.1 --- a/src/Pure/tactic.ML	Wed Feb 22 22:18:38 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Feb 22 22:18:39 2006 +0100
     1.3 @@ -642,8 +642,7 @@
     1.4  (* meta-level conjunction *)
     1.5  
     1.6  val conj_tac = SUBGOAL (fn (goal, i) =>
     1.7 -  if can Logic.dest_conjunction goal then
     1.8 -    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
     1.9 +  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
    1.10    else no_tac);
    1.11  
    1.12  val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;