# HG changeset patch
# User haftmann
# Date 1201039618 -3600
# Node ID 0929d6d08dd3547cd6a5822f2711c59af0df9a8d
# Parent  6942f3c5dec882ab85abd524f7ed7990560c6726
fixed OCaml

diff -r 6942f3c5dec8 -r 0929d6d08dd3 src/HOL/Library/Code_Index.thy
--- 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"