avoid ambiguities; tuned

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:30 2010 +0200
@@ -311,7 +311,7 @@
 lemma bind_return [simp]: "f \<guillemotright>= return = f"
   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
-lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
+lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: 'a Heap) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
@@ -410,14 +410,14 @@
 subsubsection {* SML and OCaml *}
 
 code_type Heap (SML "unit/ ->/ _")
-code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
+code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
 code_const return (SML "!(fn/ ()/ =>/ _)")
 code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
 
 code_type Heap (OCaml "unit/ ->/ _")
-code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
+code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
 code_const return (OCaml "!(fun/ ()/ ->/ _)")
-code_const Heap_Monad.raise' (OCaml "failwith/ _")
+code_const Heap_Monad.raise' (OCaml "failwith")
 
 setup {*
 
@@ -530,7 +530,7 @@
 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
 code_monad bind Haskell
 code_const return (Haskell "return")
-code_const Heap_Monad.raise' (Haskell "error/ _")
+code_const Heap_Monad.raise' (Haskell "error")
 
 hide_const (open) Heap heap guard raise' fold_map
 

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:45:29 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:45:30 2010 +0200
@@ -550,7 +550,7 @@
   }"
   unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
 thm arg_cong2
-  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
+  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = bind] split: node.split)
 
 primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
 where