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