diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Power.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -48,7 +48,7 @@
 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
 
 Goal "(n choose 0) = 1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "binomial_n_0";
 
@@ -99,7 +99,7 @@
 by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps [binomial_0]) 1);
 by (Clarify_tac 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
 				  le_Suc_eq, binomial_eq_0]));