# HG changeset patch
# User paulson
# Date 862561064 -7200
# Node ID 9366415b93ad54626d3d5d109eefe62107caabfa
# Parent  eeb4d0c7f7484c72f0a1b409a503e3608dfc978b
New blast_tac call: made possible by bug fix involving equality substitution

diff -r eeb4d0c7f748 -r 9366415b93ad src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Thu May 01 10:28:10 1997 +0200
+++ b/src/HOL/Sum.ML	Fri May 02 10:17:44 1997 +0200
@@ -123,7 +123,7 @@
 qed "sum_case_Inl";
 
 goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "sum_case_Inr";
 
 Addsimps [sum_case_Inl, sum_case_Inr];