--- a/src/HOL/WF_Rel.ML Wed Jun 18 15:30:32 1997 +0200
+++ b/src/HOL/WF_Rel.ML Wed Jun 18 15:31:31 1997 +0200
@@ -129,13 +129,8 @@
by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
by(Blast_tac 1);
be swap 1;
-by(Asm_full_simp_tac 1);
-be exE 1;
-be swap 1;
-br impI 1;
-be swap 1;
-be exE 1;
-by(rename_tac "x" 1);
+by (Asm_full_simp_tac 1);
+by (Step_tac 1);
by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
br allI 1;