diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -435,7 +435,7 @@
 				       extend_set_Un_distrib]) 2);
 by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
 by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (Blast_tac 1);
 (*The transient part*)
 by Auto_tac;
 by (force_tac (claset() addSDs [equalityD1]