diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/BExp.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
 
 subsection "Boolean Expressions"
 
-datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
 text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where