diff -r 8a15c3577770 -r b36787a56a1f src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri Jun 16 13:33:39 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri Jun 16 13:39:21 2000 +0200
@@ -534,8 +534,10 @@
 by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]);
 (*using Int_greatest actually slows the next step!*)
 by (Blast_tac 2);
-by (force_tac (claset(), 
-	      simpset() addsimps [split_extended_all]) 1);
+by (rtac ccontr 1);
+by (dtac subsetD 1);
+by (Blast_tac 1);  
+by (force_tac (claset(), simpset() addsimps [split_extended_all]) 1);
 qed "stable_project_transient";