export datatype definition which gets expanded too much in antiquotation

--- a/src/HOL/IMP/Types.thy	Tue Mar 19 14:07:13 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Tue Mar 19 14:04:53 2013 +0100
@@ -9,7 +9,9 @@
 type_synonym vname = string
 type_synonym state = "vname \<Rightarrow> val"
 
+text_raw{*\snip{aexptDef}{0}{2}{% *}
 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
+text_raw{*}%endsnip*}
 
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |