Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed HOLogic.stringT
authorkrauss
Fri, 28 Aug 2009 20:49:53 +0200
changeset 32446 cde4f2c8bdd5
parent 32445 5a03495c731a
child 32447 e78ec17718d0
fixed HOLogic.stringT
src/HOL/Tools/hologic.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle