--- a/src/ZF/OrderArith.ML Wed Jan 06 15:00:12 1999 +0100
+++ b/src/ZF/OrderArith.ML Thu Jan 07 10:56:05 1999 +0100
@@ -132,7 +132,7 @@
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
Goal "A Int B = 0 ==> \
\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
-by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
+by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")]
lam_bijective 1);
by (blast_tac (claset() addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));