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