Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

--- a/src/ZF/CardinalArith.ML	Fri Apr 28 11:24:32 1995 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Apr 28 11:31:33 1995 +0200
@@ -633,9 +633,9 @@
 
 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+by (fast_tac (ZF_cs addSIs [Ord_ordertype]) 2);
 by (rewtac Transset_def);
-by (safe_tac ZF_cs);
+by (safe_tac subset_cs);
 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1);
 by (safe_tac ZF_cs);
 by (rtac UN_I 1);

--- a/src/ZF/Coind/Map.ML	Fri Apr 28 11:24:32 1995 +0200
+++ b/src/ZF/Coind/Map.ML	Fri Apr 28 11:31:33 1995 +0200
@@ -79,19 +79,19 @@
 goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
   "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
 by (safe_tac ZF_cs);
-by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
+by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
+by (fast_tac ZF_cs 1);
 by (fast_tac ZF_cs 1);
-by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
 by (fast_tac ZF_cs 1);
+
 by (rtac (excluded_middle RS disjE) 1);
 by (etac image_Sigma1 1);
-by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
-by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
+by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
+by (asm_full_simp_tac
+ (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
 by (safe_tac FOL_cs);
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
+by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
+by (ALLGOALS (asm_full_simp_tac ZF_ss));
 by (fast_tac ZF_cs 1);
 qed "pmap_owrI";