--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Wed Sep 14 06:49:01 2011 +0200
@@ -44,10 +44,11 @@
code_pred big_step .
-values "{map t [0,1] |t. ([], \<lambda>n. 0, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
+
+values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
-(* FIXME: syntax *)
-values "{map t [0, 1, 2] |t. ([], (\<lambda>_. 3)(''x'' := 0, ''y'' := 1,''z'' := 2), 0) \<turnstile> (test_com, (%_. 0)) \<Rightarrow> t}"
-
+values "{map t [0, 1, 2] |t.
+ ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
+ \<turnstile> (test_com, <>) \<Rightarrow> t}"
end