tuned

--- a/src/HOL/IMP/Live.thy	Wed Dec 07 11:24:45 2011 +0100
+++ b/src/HOL/IMP/Live.thy	Thu Dec 08 09:10:44 2011 +0100
@@ -39,7 +39,7 @@
 by(auto simp add:L_gen_kill)
 
 lemma L_While_lpfp:
-  "\<lbrakk> vars b \<union> X \<subseteq> P; L c P \<subseteq> P \<rbrakk> \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
+  "vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
 by(simp add: L_gen_kill)