# HG changeset patch # User haftmann # Date 1201078675 -3600 # Node ID ddc6a331263695c94b230b463239d2d078f85242 # Parent f0301d6c7b7971e8aaab1a3e03ccc11f64bca48f yet another OCaml fix diff -r f0301d6c7b79 -r ddc6a3312636 src/HOL/Library/Code_Index.thy --- a/src/HOL/Library/Code_Index.thy Tue Jan 22 23:07:25 2008 +0100 +++ b/src/HOL/Library/Code_Index.thy Wed Jan 23 09:57:55 2008 +0100 @@ -214,7 +214,7 @@ code_const "op mod \ index \ index \ index" (SML "Int.mod/ ((_),/ (_))") - (OCaml "Pervasives.(mod)") + (OCaml "Pervasives.( mod )") (Haskell "mod") code_const "op = \ index \ index \ bool"