diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Thu Oct 20 09:48:00 2011 +0200 @@ -3,7 +3,7 @@ subsubsection "Dynamic Scoping of Procedures and Variables" -type_synonym penv = "name \ com" +type_synonym penv = "pname \ com" inductive big_step :: "penv \ com \ state \ state \ bool" ("_ \ _ \ _" [60,0,60] 55)