diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Live.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -7,7 +7,7 @@
 
 subsection "Liveness Analysis"
 
-fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
+fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
 "L (x ::= a) X = X-{x} \<union> vars a" |
 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
@@ -18,14 +18,14 @@
 
 value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
 
-fun "kill" :: "com \<Rightarrow> name set" where
+fun "kill" :: "com \<Rightarrow> vname set" where
 "kill SKIP = {}" |
 "kill (x ::= a) = {x}" |
 "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
 "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
 "kill (WHILE b DO c) = {}"
 
-fun gen :: "com \<Rightarrow> name set" where
+fun gen :: "com \<Rightarrow> vname set" where
 "gen SKIP = {}" |
 "gen (x ::= a) = vars a" |
 "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
@@ -94,7 +94,7 @@
 subsection "Program Optimization"
 
 text{* Burying assignments to dead variables: *}
-fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
+fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
 "bury SKIP X = SKIP" |
 "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
 "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |