1.1 --- a/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:33:27 2009 +0200
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Tue Sep 29 22:48:24 2009 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5    fun mk_new ([],[]) = Const("True",FOLogic.oT)
     1.6      | mk_new (largs,rargs) =
     1.7 -        BalancedTree.make FOLogic.mk_conj
     1.8 +        Balanced_Tree.make FOLogic.mk_conj
     1.9                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    1.10  
    1.11   val datatype_ss = @{simpset};