# HG changeset patch
# User wenzelm
# Date 1011049794 -3600
# Node ID b76a4376cfcb9d7e3a4492bbb0ee25a8f5829e10
# Parent  08bf3d911968ce40d9ae4b07565e674f02167251
added mk_conjunction_list;

diff -r 08bf3d911968 -r b76a4376cfcb src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jan 15 00:09:29 2002 +0100
+++ b/src/Pure/logic.ML	Tue Jan 15 00:09:54 2002 +0100
@@ -23,6 +23,7 @@
   val strip_prems       : int * term list * term -> term list * term
   val count_prems       : term * int -> int
   val mk_conjunction    : term * term -> term
+  val mk_conjunction_list: term list -> term
   val mk_flexpair       : term * term -> term
   val dest_flexpair     : term -> term * term
   val list_flexpairs    : (term*term)list * term -> term
@@ -124,6 +125,8 @@
 fun mk_conjunction (t, u) =
   Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0));
 
+fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
+  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
 
 
 (** flex-flex constraints **)