| changeset 32446 | cde4f2c8bdd5 |
| parent 32342 | 3fabf5b5fc83 |
| child 32657 | 5f13912245ff |
--- a/src/HOL/Tools/hologic.ML Fri Aug 28 20:22:12 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Fri Aug 28 20:49:53 2009 +0200 @@ -586,7 +586,7 @@ (* string *) -val stringT = Type ("String.string", []); +val stringT = listT charT; val mk_string = mk_list charT o map (mk_char o ord) o explode; val dest_string = implode o map (chr o dest_char) o dest_list;