# HG changeset patch
# User haftmann
# Date 1288352989 -7200
# Node ID d72f1f734e5a34d6870ab4d3b43fa14972d28cf7
# Parent  323f7aad54b0fe658695ca7127cc92fd122f646b
remove term_of equations for Heap type explicitly

diff -r 323f7aad54b0 -r d72f1f734e5a src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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"