--- a/src/HOL/MiniML/Type.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/MiniML/Type.ML Wed Aug 30 16:29:21 2000 +0200
@@ -150,7 +150,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","n")] nat_induct 1);
+by (induct_thm_tac nat_induct "n" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
@@ -161,7 +161,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
by (strip_tac 1);
by (Asm_full_simp_tac 1);
by (Simp_tac 1);
@@ -505,7 +505,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
by (strip_tac 1);
by (Asm_full_simp_tac 1);
by (Simp_tac 1);
@@ -718,7 +718,7 @@
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (rename_tac "n1" 1);
-by (res_inst_tac[("n","n1")] nat_induct 1);
+by (induct_thm_tac nat_induct "n1" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "nth_subst";