diff -r 42c1a89b45c1 -r c195f6f13769 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/logic.ML	Tue Jun 19 23:15:27 2007 +0200
@@ -19,12 +19,14 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val nth_prem: int * term -> term
+  val true_prop: term
   val conjunction: term
   val mk_conjunction: term * term -> term
   val mk_conjunction_list: term list -> term
-  val mk_conjunction_list2: term list list -> term
+  val mk_conjunction_balanced: term list -> term
   val dest_conjunction: term -> term * term
   val dest_conjunction_list: term -> term list
+  val dest_conjunction_balanced: int -> term -> term list
   val dest_conjunctions: term -> term list
   val strip_horn: term -> term list * term
   val mk_type: typ -> term
@@ -145,20 +147,24 @@
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 
+
 (** conjunction **)
 
+val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
 
+
 (*A && B*)
 fun mk_conjunction (A, B) = conjunction $ A $ B;
 
 (*A && B && C -- improper*)
-fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
+fun mk_conjunction_list [] = true_prop
   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
 
-(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
-fun mk_conjunction_list2 tss =
-  mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
+(*(A && B) && (C && D) -- balanced*)
+fun mk_conjunction_balanced [] = true_prop
+  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+
 
 (*A && B*)
 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
@@ -170,6 +176,10 @@
     NONE => [t]
   | SOME (A, B) => A :: dest_conjunction_list B);
 
+(*(A && B) && (C && D) -- balanced*)
+fun dest_conjunction_balanced 0 _ = []
+  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
+
 (*((A && B) && C) && D && E -- flat*)
 fun dest_conjunctions t =
   (case try dest_conjunction t of