src/HOL/NatDef.ML
changeset 4535 f24cebc299e4
parent 4468 d17524e0beb0
child 4599 3a4348a3d6ff
--- 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)";