# HG changeset patch
# User haftmann
# Date 1218459004 -7200
# Node ID 4e50590ea9bcaddc2ccb5fac7fab69c97a8d2621
# Parent  12254665fc41ad988d03653b6ccc493f12b1cf89
changed code setup

diff -r 12254665fc41 -r 4e50590ea9bc src/HOL/Library/Heap_Monad.thy
--- a/src/HOL/Library/Heap_Monad.thy	Mon Aug 11 14:50:02 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy	Mon Aug 11 14:50:04 2008 +0200
@@ -292,7 +292,7 @@
 
 code_type Heap (SML "unit/ ->/ _")
 code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
-code_const "op \<guillemotright>=" (SML "!(fn/ f/ =>/ fn/ g/ =>/ fn/ ()/ =>/ g/ (f/ ())/ ())")
+code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
 code_const run (SML "_")
 code_const return (SML "!(fn/ ()/ =>/ _)")
 code_const "Heap_Monad.Fail" (SML "Fail")
@@ -300,7 +300,7 @@
 
 code_type Heap (OCaml "_")
 code_const Heap (OCaml "failwith/ \"bare Heap\"")
-code_const "op \<guillemotright>=" (OCaml "!(fun/ f/ g/ ()/ ->/ g/ (f/ ())/ ())")
+code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
 code_const run (OCaml "_")
 code_const return (OCaml "!(fun/ ()/ ->/ _)")
 code_const "Heap_Monad.Fail" (OCaml "Failure")