src/ZF/ind_syntax.ML
changeset 23419 8c30dd4b3b22
parent 23156 6ec9e29143e9
child 24826 78e6a3cea367
     1.1 --- a/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:27 2007 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Tue Jun 19 23:15:38 2007 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4        fun is_ind arg = (type_of arg = iT)
     1.5    in  case List.filter is_ind (args @ cs) of
     1.6           []     => empty
     1.7 -       | u_args => fold_bal mk_Un u_args
     1.8 +       | u_args => BalancedTree.make mk_Un u_args
     1.9    end;
    1.10  
    1.11  (*univ or quniv constitutes the sum domain for mutual recursion;