diff -r 41ebc19276ea -r ba514b5aa809 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Aug 08 12:01:02 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Aug 08 14:47:24 2013 +0200
@@ -34,14 +34,11 @@
 
 subsection "Instructions and Stack Machine"
 
+text_raw{*\snip{instrdef}{0}{1}{% *}
 datatype instr = 
-  LOADI int |
-  LOAD vname |
-  ADD |
-  STORE vname |
-  JMP int |
-  JMPLESS int |
-  JMPGE int
+  LOADI int | LOAD vname | ADD | STORE vname |
+  JMP int | JMPLESS int | JMPGE int
+text_raw{*}%endsnip*}
 
 type_synonym stack = "val list"
 type_synonym config = "int \<times> state \<times> stack"