src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Thu Nov 28 10:42:19 1996 +0100
+++ b/src/ZF/ind_syntax.ML	Thu Nov 28 10:44:24 1996 +0100
@@ -97,7 +97,7 @@
                mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   in  map mk_intr constructs  end;
 
-fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
+fun mk_all_intr_tms arg = List.concat (ListPair.map mk_intr_tms arg);
 
 val Un          = Const("op Un", [iT,iT]--->iT)
 and empty       = Const("0", iT)