added ocaml strings

--- a/src/HOL/Library/ML_String.thy	Sat Sep 29 08:58:54 2007 +0200
+++ b/src/HOL/Library/ML_String.thy	Sat Sep 29 08:58:55 2007 +0200
@@ -47,6 +47,7 @@
 
 code_type ml_string
   (SML "string")
+  (OCaml "string")
   (Haskell "String")
 
 setup {*
@@ -63,6 +64,8 @@
 in
   CodeTarget.add_pretty_ml_string "SML"
     charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
+  #> CodeTarget.add_pretty_ml_string "OCaml"
+  charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
 end
 *}
 
@@ -70,12 +73,14 @@
   (Haskell "_")
 
 code_reserved SML string
+code_reserved OCaml string
 
 code_instance ml_string :: eq
   (Haskell -)
 
 code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
+  (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
 
 end

--- a/src/Tools/code/code_target.ML	Sat Sep 29 08:58:54 2007 +0200
+++ b/src/Tools/code/code_target.ML	Sat Sep 29 08:58:55 2007 +0200
@@ -1640,7 +1640,7 @@
   ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
       pretty_string = ML_Syntax.print_string,
       pretty_numeral = fn unbounded => fn k =>
-        if unbounded then "(" ^ string_of_int k ^ " : int)"
+        if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
         else string_of_int k,
       pretty_list = Pretty.enum "," "[" "]",
       infix_cons = (7, "::")}),
@@ -1650,7 +1650,7 @@
             then prefix "\\" (string_of_int i)
             else c
           end),
-      pretty_string = (fn _ => error "OCaml: no pretty strings"),
+      pretty_string = ML_Syntax.print_string,
       pretty_numeral = fn unbounded => fn k => if k >= 0 then
             if unbounded then
               "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"