src/ZF/Datatype.ML
changeset 7693 c3e0c26e7d6f
parent 6141 a6922171b396
child 9000 c20d58286a51
--- 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)));