src/HOL/List.thy

--- a/src/HOL/List.thy	Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/List.thy	Fri May 23 16:41:39 2008 +0200
@@ -3410,7 +3410,7 @@
     val i = HOLogic.dest_char t;
     val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
       (gr, fastype_of t)
-  in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i)))
+  in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
   end handle TERM _ => NONE;
 
 in