FOLogic.mk_conj;
authorwenzelm
Mon, 04 Oct 1999 21:37:00 +0200
changeset 7693 c3e0c26e7d6f
parent 7692 89bbce6f5c17
child 7694 20121c9dc1a6
FOLogic.mk_conj;
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)));