# HG changeset patch
# User wenzelm
# Date 1135347409 -3600
# Node ID 8b1a4e8ed1996480dc6284a8267d8bcbe6c2540e
# Parent  567370efb6d7f623e8af0456dbca1a7df7fc0cda
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;

diff -r 567370efb6d7 -r 8b1a4e8ed199 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Dec 23 15:16:48 2005 +0100
+++ b/src/Pure/tactic.ML	Fri Dec 23 15:16:49 2005 +0100
@@ -98,8 +98,8 @@
   val instantiate_tac   : (string * string) list -> tactic
   val thin_tac          : string -> int -> tactic
   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
-  val CONJUNCTS: int -> tactic -> int -> tactic
-  val CONJUNCTS2: int -> tactic -> int -> tactic
+  val CONJUNCTS: tactic -> int -> tactic
+  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
 end;
 
 signature TACTIC =
@@ -650,15 +650,16 @@
       | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
   in TRY oo tac end;
 
-(*treat conjuncts as separate sub-goals*)
-fun CONJUNCTS n tac =
+fun CONJUNCTS tac =
+  SELECT_GOAL (conjunction_tac 1
+    THEN tac
+    THEN PRIMITIVE Drule.conj_curry);
+
+fun PRECISE_CONJUNCTS n tac =
   SELECT_GOAL (precise_conjunction_tac n 1
     THEN tac
     THEN PRIMITIVE Drule.conj_curry);
 
-(*treat two levels of conjunctions*)
-fun CONJUNCTS2 n tac = CONJUNCTS n (ALLGOALS (CONJUNCTS ~1 tac));
-
 end;
 
 structure BasicTactic: BASIC_TACTIC = Tactic;