src/Pure/conjunction.ML

   val conjunctionD2: thm
   val conjunctionI: thm
   val intr: thm -> thm -> thm
   val intr_balanced: thm list -> thm
   val elim: thm -> thm * thm
+  val elim_conjunctions: thm -> thm list
   val elim_balanced: int -> thm -> thm list
   val curry_balanced: int -> thm -> thm
   val uncurry_balanced: int -> thm -> thm
 end;
 

     Thm.implies_elim (inst conjunctionD2) th)
   end;
 
 end;
 
+fun elim_conjunctions th =
+  (case try elim th of
+    NONE => [th]
+  | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
+
 
 (* balanced conjuncts *)
 
 fun intr_balanced [] = asm_rl
   | intr_balanced ths = Balanced_Tree.make (uncurry intr) ths;