diff -r cb3612cc41a3 -r fc075ae929e4 src/ZF/UNITY/FP.thy
--- a/src/ZF/UNITY/FP.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/ZF/UNITY/FP.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -37,15 +37,13 @@
 done
 
 lemma stable_FP_Orig_Int: "F \<in> program ==> F \<in> stable(FP_Orig(F) Int B)"
-apply (unfold FP_Orig_def stable_def)
-apply (subst Int_Union2)
+apply (simp only: FP_Orig_def stable_def Int_Union2)
 apply (blast intro: constrains_UN)
 done
 
 lemma FP_Orig_weakest2: 
     "[| \<forall>B. F \<in> stable (A Int B); st_set(A) |]  ==> A \<subseteq> FP_Orig(F)"
-apply (unfold FP_Orig_def stable_def st_set_def, blast)
-done
+by (unfold FP_Orig_def stable_def st_set_def, blast)
 
 lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard]