--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 12 15:51:25 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 12 16:19:05 2013 +0200
@@ -274,10 +274,8 @@
Some (x, h') \<Rightarrow> execute (g x) h'
| None \<Rightarrow> None)"
-setup {*
- Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind Heap_Monad.bind
lemma execute_bind [execute_simps]:
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"