--- a/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -12,12 +12,12 @@
 Addsimps g.simps;
 
 Goal "g x < Suc x";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
 by Auto_tac;
 qed "g_terminates";
 
 Goal "g x = 0";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
 qed "g_zero";