# HG changeset patch
# User wenzelm
# Date 1135347408 -3600
# Node ID 567370efb6d7f623e8af0456dbca1a7df7fc0cda
# Parent  466351242c6fba90efb7dd59b78c5a56e14012d4
added mk_conjunction_list2;

diff -r 466351242c6f -r 567370efb6d7 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Dec 23 15:16:46 2005 +0100
+++ b/src/Pure/logic.ML	Fri Dec 23 15:16:48 2005 +0100
@@ -23,6 +23,7 @@
   val nth_prem: int * term -> term
   val mk_conjunction: term * term -> term
   val mk_conjunction_list: term list -> term
+  val mk_conjunction_list2: term list list -> term
   val dest_conjunction: term -> term * term
   val dest_conjunctions: term -> term list
   val strip_horn: term -> term list * term
@@ -131,13 +132,20 @@
 
 (** conjunction **)
 
+(*A && B*)
 fun mk_conjunction (t, u) =
   Term.list_all ([("X", propT)],
     mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
 
+(*A && B && C -- improper*)
 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   | 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*)
 fun dest_conjunction
       (t as Const ("all", _) $ Abs (_, _,
         Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
@@ -146,6 +154,7 @@
       else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
 
+(*((A && B) && C) && D && E -- flat*)
 fun dest_conjunctions t =
   (case try dest_conjunction t of
     NONE => [t]