src/Pure/tactic.ML
changeset 19185 9fb741abb008
parent 19125 59b26248547b
child 19423 51eeee99bd8f
     1.1 --- a/src/Pure/tactic.ML	Sat Mar 04 21:10:08 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sat Mar 04 21:10:09 2006 +0100
     1.3 @@ -657,12 +657,12 @@
     1.4  fun CONJUNCTS tac =
     1.5    SELECT_GOAL (conjunction_tac 1
     1.6      THEN tac
     1.7 -    THEN PRIMITIVE Drule.conj_curry);
     1.8 +    THEN PRIMITIVE (Drule.conj_uncurry ~1));
     1.9  
    1.10  fun PRECISE_CONJUNCTS n tac =
    1.11    SELECT_GOAL (precise_conjunction_tac n 1
    1.12      THEN tac
    1.13 -    THEN PRIMITIVE Drule.conj_curry);
    1.14 +    THEN PRIMITIVE (Drule.conj_uncurry ~1));
    1.15  
    1.16  end;
    1.17