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