src/ZF/Datatype_ZF.thy

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