--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Jan 01 14:44:52 2016 +0100
@@ -110,7 +110,7 @@
subarray_def rev.simps[where j=0] elim!: effect_elims)
(drule sym[of "List.length (Array.get h a)"], simp)
-definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
+definition "example = (Array.make 10 id \<bind> (\<lambda>a. rev a 0 9))"
export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp