changeset 23419 | 8c30dd4b3b22 |
parent 23156 | 6ec9e29143e9 |
child 24826 | 78e6a3cea367 |
--- 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;