author | wenzelm |
Sat, 04 Mar 2006 21:10:09 +0100 | |
changeset 19185 | 9fb741abb008 |
parent 19184 | 3e30297e1300 |
child 19186 | 1bf4b5c4a794 |
--- a/src/Pure/tactic.ML Sat Mar 04 21:10:08 2006 +0100 +++ b/src/Pure/tactic.ML Sat Mar 04 21:10:09 2006 +0100 @@ -657,12 +657,12 @@ fun CONJUNCTS tac = SELECT_GOAL (conjunction_tac 1 THEN tac - THEN PRIMITIVE Drule.conj_curry); + THEN PRIMITIVE (Drule.conj_uncurry ~1)); fun PRECISE_CONJUNCTS n tac = SELECT_GOAL (precise_conjunction_tac n 1 THEN tac - THEN PRIMITIVE Drule.conj_curry); + THEN PRIMITIVE (Drule.conj_uncurry ~1)); end;