diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/NatDef.ML	Thu Jan 08 18:09:07 1998 +0100
@@ -135,11 +135,11 @@
 (*** nat_case -- the selection operator for nat ***)
 
 goalw thy [nat_case_def] "nat_case a f 0 = a";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
 qed "nat_case_0";
 
 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
 qed "nat_case_Suc";
 
 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";