--- a/src/HOL/Library/Code_Index.thy Tue Jan 22 11:37:28 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy Tue Jan 22 23:06:58 2008 +0100
@@ -194,7 +194,7 @@
code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
(SML "Int.+/ ((_),/ (_))")
- (OCaml "Pervasives.+")
+ (OCaml "Pervasives.(+)")
(Haskell infixl 6 "+")
code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
@@ -204,17 +204,17 @@
code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
(SML "Int.*/ ((_),/ (_))")
- (OCaml "Pervasives.*")
+ (OCaml "Pervasives.(*)")
(Haskell infixl 7 "*")
code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
(SML "Int.div/ ((_),/ (_))")
- (OCaml "Pervasives.div")
+ (OCaml "Pervasives.(/)")
(Haskell "div")
code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
(SML "Int.mod/ ((_),/ (_))")
- (OCaml "Pervasives.mod")
+ (OCaml "Pervasives.(mod)")
(Haskell "mod")
code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"