diff -r 51692ec1b220 -r 1cb90bbbf45e src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Mon Feb 22 09:15:11 2010 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Feb 22 09:15:12 2010 +0100
@@ -58,9 +58,8 @@
 apply (rule monoI)
 apply (unfold prefix_def)
 apply (erule genPrefix.induct, auto)
-apply (simp add: union_le_mono)
 apply (erule order_trans)
-apply (rule union_upper1)
+apply simp
 done
 
 (** setsum **)