added dest_conjunctions (cf. Logic.dest_conjunctions);

--- a/src/Pure/conjunction.ML	Tue Mar 31 20:40:25 2009 +0200
+++ b/src/Pure/conjunction.ML	Tue Mar 31 21:31:04 2009 +0200
@@ -10,6 +10,7 @@
   val mk_conjunction: cterm * cterm -> cterm
   val mk_conjunction_balanced: cterm list -> cterm
   val dest_conjunction: cterm -> cterm * cterm
+  val dest_conjunctions: cterm -> cterm list
   val cong: thm -> thm -> thm
   val convs: (cterm -> thm) -> cterm -> thm
   val conjunctionD1: thm
@@ -44,6 +45,11 @@
     (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
   | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
 
+fun dest_conjunctions ct =
+  (case try dest_conjunction ct of
+    NONE => [ct]
+  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
+
 
 
 (** derived rules **)