src/HOL/ex/Recdef.ML

--- a/src/HOL/ex/Recdef.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/ex/Recdef.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -38,9 +38,9 @@
 (* proving the termination condition: *)
 val [tc] = mapf.tcs;
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-br allI 1;
-by(case_tac "n=0" 1);
-by(ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (case_tac "n=0" 1);
+by (ALLGOALS Asm_simp_tac);
 val lemma = result();
 
 (* removing the termination condition from the generated thms: *)