1.1 --- a/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:13 2011 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Mon Jun 06 16:29:38 2011 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  values
     1.5    "{(i,map t [''x'',''y''],stk) | i t stk.
     1.6      [LOAD ''y'', STORE ''x''] \<turnstile>
     1.7 -    (0,lookup[(''x'',3),(''y'',4)],[]) \<rightarrow>* (i,t,stk)}"
     1.8 +    (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}"
     1.9  
    1.10  
    1.11  subsection{* Verification infrastructure *}