changeset 32765 | 3032c0308019 |
parent 32740 | 9dd0a2f83429 |
child 35409 | 5c5bb83f2bae |
--- a/src/ZF/Datatype_ZF.thy Tue Sep 29 22:33:27 2009 +0200 +++ b/src/ZF/Datatype_ZF.thy Tue Sep 29 22:48:24 2009 +0200 @@ -63,7 +63,7 @@ fun mk_new ([],[]) = Const("True",FOLogic.oT) | mk_new (largs,rargs) = - BalancedTree.make FOLogic.mk_conj + Balanced_Tree.make FOLogic.mk_conj (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); val datatype_ss = @{simpset};