--- a/src/HOL/Library/MLString.thy Fri Mar 30 16:19:00 2007 +0200
+++ b/src/HOL/Library/MLString.thy Fri Mar 30 16:19:01 2007 +0200
@@ -67,14 +67,17 @@
code_reserved SML string explode
+code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
+ (SML "!((_ : string) = _)")
+ (Haskell infixl 4 "==")
+
+code_instance ml_string :: eq (Haskell -)
+
text {* disable something ugly *}
code_const "ml_string_rec" and "ml_string_case" and "size \<Colon> ml_string \<Rightarrow> nat"
(SML "!((_); (_); raise Fail \"ml'_string'_rec\")"
and "!((_); (_); raise Fail \"ml'_string'_case\")"
and "!((_); raise Fail \"size'_ml'_string\")")
- (OCaml "!((_); (_); failwith \"ml'_string'_rec\")"
- and "!((_); (_); failwith \"ml'_string'_case\")"
- and "!((_); failwith \"size'_ml'_string\")")
end