src/HOL/Tools/hologic.ML
changeset 40627 becf5d5187cc
parent 39756 6c8e83d94536
child 40845 15b97bd4b5c0
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -598,7 +598,7 @@
     1.4  
     1.5  val stringT = listT charT;
     1.6  
     1.7 -val mk_string = mk_list charT o map (mk_char o ord) o explode;
     1.8 +val mk_string = mk_list charT o map (mk_char o ord) o raw_explode;
     1.9  val dest_string = implode o map (chr o dest_char) o dest_list;
    1.10  
    1.11