src/HOL/IMP/Fold.thy

 theory Fold imports Sem_Equiv begin
 
 subsection "Simple folding of arithmetic expressions"
 
 type_synonym
-  tab = "name \<Rightarrow> val option"
+  tab = "vname \<Rightarrow> val option"
 
 (* maybe better as the composition of substitution and the existing simp_const(0) *)
 fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
 "simp_const (N n) _ = N n" |
 "simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |

      (auto simp: approx_def split: aexp.splits option.splits)
 
 definition
   "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
 
-primrec lnames :: "com \<Rightarrow> name set" where
+primrec lnames :: "com \<Rightarrow> vname set" where
 "lnames SKIP = {}" |
 "lnames (x ::= a) = {x}" |
 "lnames (c1; c2) = lnames c1 \<union> lnames c2" |
 "lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
 "lnames (WHILE b DO c) = lnames c"