diff -r 0130ad32a612 -r 56f269baae76 src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Sun Nov 04 17:36:26 2012 +0100
+++ b/src/HOL/IMP/ASM.thy	Sun Nov 04 18:38:18 2012 +0100
@@ -32,8 +32,7 @@
 "exec (i#is) s stk = exec is s (exec1 i s stk)"
 text_raw{*}%endsnip*}
 
-value "exec [LOADI 5, LOAD ''y'', ADD]
- <''x'' := 42, ''y'' := 43> [50]"
+value "exec [LOADI 5, LOAD ''y'', ADD] <''x'' := 42, ''y'' := 43> [50]"
 
 lemma exec_append[simp]:
   "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"