diff -r cb3612cc41a3 -r fc075ae929e4 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -284,8 +284,10 @@
 apply (rule_tac [2] mono_length)
     prefer 3 apply simp
 apply (simp_all add: refl_prefix Le_def comp_def length_type)
-apply (subst Int_commute)
-apply (rule_tac A = " ({s \<in> state . k \<le> length (s ` rel) } \<inter> {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length (s`rel) }" in LeadsTo_weaken_L)
+apply (subst Int_commute [of _ "{x \<in> state . n < x ` NbR}"])
+apply (rule_tac A = "({s \<in> state . k \<le> length (s ` rel) } \<inter>
+                      {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length(s`rel)}"
+       in LeadsTo_weaken_L)
 apply (rule PSP_Stable, safe)
 apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
 apply (rule_tac [2] LeadsTo_weaken)