diff -r c195f6f13769 -r 8c30dd4b3b22 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:27 2007 +0200
+++ b/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:38 2007 +0200
@@ -114,7 +114,7 @@
       fun is_ind arg = (type_of arg = iT)
   in  case List.filter is_ind (args @ cs) of
          []     => empty
-       | u_args => fold_bal mk_Un u_args
+       | u_args => BalancedTree.make mk_Un u_args
   end;
 
 (*univ or quniv constitutes the sum domain for mutual recursion;