diff -r 96fcfbfa4fb5 -r a14e5451f613 src/HOL/WF_Rel.ML
--- 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;