--- 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 **)