--- a/src/HOL/Induct/Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
typedecl loc
type_synonym state = "loc => nat"
-datatype_new
+datatype
exp = N nat
| X loc
| Op "nat => nat => nat" exp exp