src/Pure/tactic.ML
changeset 19423 51eeee99bd8f
parent 19185 9fb741abb008
child 19473 d87a8838afa4
     1.1 --- a/src/Pure/tactic.ML	Thu Apr 13 12:01:00 2006 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Apr 13 12:01:01 2006 +0200
     1.3 @@ -642,7 +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 rtac Drule.conjunctionI i
     1.8 +  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
     1.9    else no_tac);
    1.10  
    1.11  val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
    1.12 @@ -657,12 +657,12 @@
    1.13  fun CONJUNCTS tac =
    1.14    SELECT_GOAL (conjunction_tac 1
    1.15      THEN tac
    1.16 -    THEN PRIMITIVE (Drule.conj_uncurry ~1));
    1.17 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
    1.18  
    1.19  fun PRECISE_CONJUNCTS n tac =
    1.20    SELECT_GOAL (precise_conjunction_tac n 1
    1.21      THEN tac
    1.22 -    THEN PRIMITIVE (Drule.conj_uncurry ~1));
    1.23 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
    1.24  
    1.25  end;
    1.26