src/HOL/Library/MLString.thy

--- a/src/HOL/Library/MLString.thy	Wed Aug 30 12:28:39 2006 +0200
+++ b/src/HOL/Library/MLString.thy	Wed Aug 30 15:11:17 2006 +0200
@@ -76,7 +76,7 @@
     end;
   val print_string = quote;
 in 
-  CodegenPackage.add_pretty_ml_string "ml" "Nil" "Cons" "STR"
+  CodegenPackage.add_pretty_ml_string "ml" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
     print_char print_string "String.implode"
 end
 *}