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. - (\p. SKIP) \ (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \ t}" + (\p. SKIP) \ (CALL ''p'', <''x'' := 42, ''y'' := 43>) \ t}" -values "{map t [''x'',''y'',''z''] |t. (\p. SKIP) \ (test_com, (%_. 0)) \ t}" +values "{map t [''x'',''y'',''z''] |t. (\p. SKIP) \ (test_com, <>) \ t}" end