diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Induct/Com.thy
--- 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