# HG changeset patch
# User wenzelm
# Date 1238527864 -7200
# Node ID eb99b9134f2e23b7010e786e8eafc76564056902
# Parent  8aac4b9742804b5221034c700a8770d801c3c379
added dest_conjunctions (cf. Logic.dest_conjunctions);

diff -r 8aac4b974280 -r eb99b9134f2e src/Pure/conjunction.ML
--- 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 **)