diff -r 352c73a689da -r c3d6e570ccef src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -405,7 +405,7 @@
 qed
 
 interpretation heap!: partial_function_definitions Heap_ord Heap_lub
-  where "Heap_lub {} \<equiv> Heap Map.empty"
+  rewrites "Heap_lub {} \<equiv> Heap Map.empty"
 by (fact heap_interpretation)(simp add: Heap_lub_empty)
 
 lemma heap_step_admissible: