--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 20:51:36 2014 +0200
@@ -16,7 +16,7 @@
text {* Monadic heap actions either produce values
and transform the heap, or fail *}
-datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
+datatype_new 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
lemma [code, code del]:
"(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"