src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Tue Nov 26 16:07:17 1996 +0100
+++ b/src/ZF/ind_syntax.ML	Tue Nov 26 16:11:18 1996 +0100
@@ -97,7 +97,7 @@
                mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
   in  map mk_intr constructs  end;
 
-val mk_all_intr_tms = flat o map mk_intr_tms o op ~~;
+fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
 
 val Un          = Const("op Un", [iT,iT]--->iT)
 and empty       = Const("0", iT)