1.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
     1.3 @@ -277,10 +277,10 @@
     1.4  text {* OCaml *}
     1.5  
     1.6  code_type ref (OCaml "_/ ref")
     1.7 -code_const Ref (OCaml "failwith/ \"bare Ref\")")
     1.8 -code_const ref (OCaml "(fn/ ()/ =>/ ref/ _)")
     1.9 -code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
    1.10 -code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
    1.11 +code_const Ref (OCaml "failwith/ \"bare Ref\"")
    1.12 +code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)")
    1.13 +code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
    1.14 +code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
    1.15  
    1.16  code_reserved OCaml ref
    1.17