--- a/src/HOL/IMP/ASM.thy Thu Oct 20 22:26:02 2011 +0200 +++ b/src/HOL/IMP/ASM.thy Fri Oct 21 08:25:04 2011 +0200 @@ -4,7 +4,7 @@ subsection "Arithmetic Stack Machine" -datatype ainstr = LOADI val | LOAD string | ADD +datatype ainstr = LOADI val | LOAD vname | ADD type_synonym stack = "val list"