src/HOL/NanoJava/State.thy

--- a/src/HOL/NanoJava/State.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/NanoJava/State.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
 text {* Locations, i.e.\ abstract references to objects *}
 typedecl loc 
 
-datatype val
+datatype_new val
   = Null        --{* null reference *}
   | Addr loc    --{* address, i.e. location of object *}