--- 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