# HG changeset patch
# User kleing
# Date 1320304213 -39600
# Node ID df7554ebe02471aa1a32eaab4ea046f610ed5001
# Parent  654cc47f6115032028ac415049809dbab1bb99c1
string -> vname

diff -r 654cc47f6115 -r df7554ebe024 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Nov 03 16:22:29 2011 +1100
+++ b/src/HOL/IMP/Compiler.thy	Thu Nov 03 18:10:13 2011 +1100
@@ -32,10 +32,10 @@
 subsection "Instructions and Stack Machine"
 
 datatype instr = 
-  LOADI int | 
-  LOAD string | 
+  LOADI int |
+  LOAD vname |
   ADD |
-  STORE string |
+  STORE vname |
   JMP int |
   JMPLESS int |
   JMPGE int