# HG changeset patch
# User wenzelm
# Date 939065855 -7200
# Node ID 20121c9dc1a6db0bff28e138ac64ef583ad02aad
# Parent  c3e0c26e7d6f546839ba0067ea17b6d65b3ec897
tryres, gen_make_elim moved here;

diff -r c3e0c26e7d6f -r 20121c9dc1a6 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Mon Oct 04 21:37:00 1999 +0200
+++ b/src/ZF/ind_syntax.ML	Mon Oct 04 21:37:35 1999 +0200
@@ -101,8 +101,9 @@
 
 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);
 
@@ -112,7 +113,7 @@
       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;
@@ -151,9 +152,18 @@
                 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;