--- a/src/HOL/Sum.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/Sum.ML Thu Jan 08 18:09:07 1998 +0100
@@ -119,11 +119,11 @@
(** sum_case -- the selection operator for sums **)
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sum_case_Inl";
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sum_case_Inr";
Addsimps [sum_case_Inl, sum_case_Inr];