# HG changeset patch
# User krauss
# Date 1251485393 -7200
# Node ID cde4f2c8bdd53083a3e271a37e1a5b4dfa829692
# Parent  5a03495c731a43cf045e5984e0a73c9a25b0e1f0
fixed HOLogic.stringT

diff -r 5a03495c731a -r cde4f2c8bdd5 src/HOL/Tools/hologic.ML
--- 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;