diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs_Stat_Vars_Stat.thy --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Thu Oct 20 09:48:00 2011 +0200 @@ -4,9 +4,9 @@ subsubsection "Static Scoping of Procedures and Variables" type_synonym addr = nat -type_synonym venv = "name \ addr" +type_synonym venv = "vname \ addr" type_synonym store = "addr \ val" -type_synonym penv = "(name \ com \ venv) list" +type_synonym penv = "(pname \ com \ venv) list" fun venv :: "penv \ venv \ nat \ venv" where "venv(_,ve,_) = ve"