diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/VC.thy --- a/src/HOL/IMP/VC.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/VC.thy Thu Oct 20 09:48:00 2011 +0200 @@ -8,7 +8,7 @@ invariants. *} datatype acom = Askip - | Aassign name aexp + | Aassign vname aexp | Asemi acom acom | Aif bexp acom acom | Awhile bexp assn acom