diff -r 690f9cccf232 -r 3032c0308019 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Sep 29 22:33:27 2009 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Sep 29 22:48:24 2009 +0200
@@ -99,7 +99,7 @@
       fun is_ind arg = (type_of arg = iT)
   in  case List.filter is_ind (args @ cs) of
          []     => @{const 0}
-       | u_args => BalancedTree.make mk_Un u_args
+       | u_args => Balanced_Tree.make mk_Un u_args
   end;