--- a/src/HOL/Library/Heap_Monad.thy Sun Apr 27 17:13:01 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy Mon Apr 28 13:41:04 2008 +0200
@@ -299,9 +299,8 @@
subsubsection {* SML *}
code_type Heap (SML "unit/ ->/ _")
-term "op \<guillemotright>="
code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
-code_monad run "op \<guillemotright>=" "()" SML
+code_monad run "op \<guillemotright>=" return "()" SML
code_const run (SML "_")
code_const return (SML "(fn/ ()/ =>/ _)")
code_const "Heap_Monad.Fail" (SML "Fail")
@@ -312,7 +311,7 @@
code_type Heap (OCaml "_")
code_const Heap (OCaml "failwith/ \"bare Heap\"")
-code_monad run "op \<guillemotright>=" "()" OCaml
+code_monad run "op \<guillemotright>=" return "()" OCaml
code_const run (OCaml "_")
code_const return (OCaml "(fn/ ()/ =>/ _)")
code_const "Heap_Monad.Fail" (OCaml "Failure")