--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 11:35:28 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 13:49:49 2010 +0200
@@ -16,6 +16,10 @@
and transform the heap, or fail *}
datatype '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"
+ ..
+
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
[code del]: "execute (Heap f) = f"