tuned conj_curry;
authorwenzelm
Sat, 04 Mar 2006 21:10:09 +0100
changeset 19185 9fb741abb008
parent 19184 3e30297e1300
child 19186 1bf4b5c4a794
tuned conj_curry;
src/Pure/tactic.ML
--- 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;