diff -r 884d27ede438 -r b80108b346a9 src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -31,10 +31,9 @@
 
 code_pred big_step .
 
-(* FIXME: example state syntax *)
 values "{map t [''x'',''y'',''z''] |t. 
-          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}"
+          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
 
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
+values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end