# HG changeset patch
# User bulwahn
# Date 1305821360 -7200
# Node ID 1e1b74448f6bfecd107db567a9a495cf43eab4e0
# Parent  9eef1dc200a81837a7ffd4ae10fa6ebec19efa98
a deeper understanding of the code generation adaptation compared to 9079f49053e5

diff -r 9eef1dc200a8 -r 1e1b74448f6b src/HOL/Library/Code_Char_ord.thy
--- a/src/HOL/Library/Code_Char_ord.thy	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Library/Code_Char_ord.thy	Thu May 19 18:09:20 2011 +0200
@@ -10,14 +10,14 @@
   
 code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) <= _)")
-  (OCaml "<=")
+  (OCaml "!((_ : char) <= _)")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
   (Eval infixl 6 "<=")
 
 code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) < _)")
-  (OCaml "<")
+  (OCaml "!((_ : char) < _)")
   (Haskell infix 4 "<")
   (Scala infixl 4 "<")
   (Eval infixl 6 "<")