# HG changeset patch
# User nipkow
# Date 1363698433 -3600
# Node ID a5af7c2baf2b1cbff5410b9d1e90793e46d025d6
# Parent  bc3651180a09eef8a6ea9cc92307f01faaac1de4
tuned

diff -r bc3651180a09 -r a5af7c2baf2b src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Tue Mar 19 13:19:21 2013 +0100
+++ b/src/HOL/IMP/Live_True.thy	Tue Mar 19 14:07:13 2013 +0100
@@ -9,7 +9,7 @@
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = 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 (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (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)"