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