--- a/src/HOL/IMP/Live_True.thy Sat Mar 16 10:50:23 2013 +0100
+++ b/src/HOL/IMP/Live_True.thy Sat Mar 16 17:22:05 2013 +0100
@@ -8,7 +8,7 @@
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
-"L (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
+"L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"