diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/String.thy --- a/src/HOL/String.thy Sat Feb 13 23:16:06 2010 +0100 +++ b/src/HOL/String.thy Sat Feb 13 23:24:57 2010 +0100 @@ -79,7 +79,7 @@ "_String" :: "xstr => string" ("_") use "Tools/string_syntax.ML" -setup StringSyntax.setup +setup String_Syntax.setup definition chars :: string where "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,