# HG changeset patch
# User nipkow
# Date 1319178304 -7200
# Node ID 62ca94616539dedbd941e8f1c7c1454d0d1bce74
# Parent  3eadb9b6a05500d307463db2a2506794a052010f# Parent  6eab55bab82f346d9d3ac4f57a9f35b2f865b726
merged

diff -r 3eadb9b6a055 -r 62ca94616539 src/HOL/IMP/ASM.thy
--- 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"