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