1.1 --- a/src/Pure/conjunction.ML	Tue Mar 31 20:40:25 2009 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Tue Mar 31 21:31:04 2009 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val mk_conjunction: cterm * cterm -> cterm
     1.5    val mk_conjunction_balanced: cterm list -> cterm
     1.6    val dest_conjunction: cterm -> cterm * cterm
     1.7 +  val dest_conjunctions: cterm -> cterm list
     1.8    val cong: thm -> thm -> thm
     1.9    val convs: (cterm -> thm) -> cterm -> thm
    1.10    val conjunctionD1: thm
    1.11 @@ -44,6 +45,11 @@
    1.12      (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
    1.13    | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
    1.14  
    1.15 +fun dest_conjunctions ct =
    1.16 +  (case try dest_conjunction ct of
    1.17 +    NONE => [ct]
    1.18 +  | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
    1.19 +
    1.20  
    1.21  
    1.22  (** derived rules **)