src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/ZF/ind_syntax.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -96,8 +96,8 @@
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = iT)
-  in  case List.filter is_ind (args @ cs) of
-         []     => @{const 0}
+  in  case filter is_ind (args @ cs) of
+         [] => @{const 0}
        | u_args => Balanced_Tree.make mk_Un u_args
   end;