src/HOL/Tools/hologic.ML

   | dest_char t = raise TERM ("dest_char", [t]);
 
 
 (* 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;