src/ZF/ind_syntax.ML
changeset 32765 3032c0308019
parent 32740 9dd0a2f83429
child 32952 aeb1e44fbc19
--- 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;