src/ZF/ind_syntax.ML

 	               $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
 
-val Un          = Const("op Un", [iT,iT]--->iT)
-and empty       = Const("0", iT)
+fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
+
+val empty       = Const("0", iT)
 and univ        = Const("Univ.univ", iT-->iT)
 and quniv       = Const("QUniv.quniv", iT-->iT);
 
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = iT)
   in  case filter is_ind (args @ cs) of
          []     => empty
-       | u_args => fold_bal (app Un) u_args
+       | u_args => fold_bal mk_Un u_args
   end;
 
 (*univ or quniv constitutes the sum domain for mutual recursion;
   it is applied to the datatype parameters and to Consts occurring in the
   definition other than Nat.nat and the datatype sets themselves.

 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
                 Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
                 make_elim succ_inject, 
                 refl_thin, conjE, exE, disjE];
 
+
+(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
+fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
+  | tryres (th, []) = raise THM("tryres", 0, [th]);
+
+fun gen_make_elim elim_rls rl = 
+      standard (tryres (rl, elim_rls @ [revcut_rl]));
+
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
+
 
 end;
 
 
 (*For convenient access by the user*)