src/HOL/IMP/ASM.thy
changeset 45222 6eab55bab82f
parent 45015 fdac1e9880eb
child 45257 12063e071d92
--- a/src/HOL/IMP/ASM.thy	Thu Oct 20 10:44:00 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Fri Oct 21 08:24:57 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"