diff -r 12b94d7f7e1f -r e086b4e846b8 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Fri Jan 05 14:31:44 2007 +0100
+++ b/src/HOL/Library/MLString.thy	Fri Jan 05 14:31:45 2007 +0100
@@ -75,4 +75,14 @@
 
 code_reserved SML string explode
 
+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