# HG changeset patch
# User wenzelm
# Date 939065820 -7200
# Node ID c3e0c26e7d6f546839ba0067ea17b6d65b3ec897
# Parent  89bbce6f5c17b275d3ad0e86fa21d5956b8a0098
FOLogic.mk_conj;

diff -r 89bbce6f5c17 -r c3e0c26e7d6f src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Mon Oct 04 21:35:26 1999 +0200
+++ b/src/ZF/Datatype.ML	Mon Oct 04 21:37:00 1999 +0200
@@ -59,7 +59,7 @@
 
   fun mk_new ([],[]) = Const("True",FOLogic.oT)
     | mk_new (largs,rargs) =
-	fold_bal (app FOLogic.conj) 
+	fold_bal FOLogic.mk_conj
 		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));