1.1 --- a/src/HOL/IMP/Live.thy	Wed Oct 19 23:07:48 2011 +0200
     1.2 +++ b/src/HOL/IMP/Live.thy	Thu Oct 20 09:48:00 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  subsection "Liveness Analysis"
     1.6  
     1.7 -fun L :: "com \<Rightarrow> name set \<Rightarrow> name set" where
     1.8 +fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
     1.9  "L SKIP X = X" |
    1.10  "L (x ::= a) X = X-{x} \<union> vars a" |
    1.11  "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
    1.12 @@ -18,14 +18,14 @@
    1.13  
    1.14  value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
    1.15  
    1.16 -fun "kill" :: "com \<Rightarrow> name set" where
    1.17 +fun "kill" :: "com \<Rightarrow> vname set" where
    1.18  "kill SKIP = {}" |
    1.19  "kill (x ::= a) = {x}" |
    1.20  "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
    1.21  "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
    1.22  "kill (WHILE b DO c) = {}"
    1.23  
    1.24 -fun gen :: "com \<Rightarrow> name set" where
    1.25 +fun gen :: "com \<Rightarrow> vname set" where
    1.26  "gen SKIP = {}" |
    1.27  "gen (x ::= a) = vars a" |
    1.28  "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
    1.29 @@ -94,7 +94,7 @@
    1.30  subsection "Program Optimization"
    1.31  
    1.32  text{* Burying assignments to dead variables: *}
    1.33 -fun bury :: "com \<Rightarrow> name set \<Rightarrow> com" where
    1.34 +fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
    1.35  "bury SKIP X = SKIP" |
    1.36  "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
    1.37  "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |