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