# HG changeset patch
# User haftmann
# Date 1279118730 -7200
# Node ID 01d308b00bcfe508ce65e49343f6e0cbdb13616b
# Parent  11f813e86305af25566b96b07d28d83ea70a8094
repaired reference implementation for OCaml

diff -r 11f813e86305 -r 01d308b00bcf src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
@@ -277,10 +277,10 @@
 text {* OCaml *}
 
 code_type ref (OCaml "_/ ref")
-code_const Ref (OCaml "failwith/ \"bare Ref\")")
-code_const ref (OCaml "(fn/ ()/ =>/ ref/ _)")
-code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
-code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
+code_const Ref (OCaml "failwith/ \"bare Ref\"")
+code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)")
+code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
+code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
 
 code_reserved OCaml ref