1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 06 14:47:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 06 14:47:58 2010 +0100
     1.3 @@ -133,8 +133,9 @@
     1.4        Type (s, _) =>
     1.5        let val s' = shortest_name s in
     1.6          prefix ^
     1.7 -        (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
     1.8 -        atom_suffix s m
     1.9 +        (if T = @{typ string} then "s"
    1.10 +         else if String.isPrefix "\\" s' then s'
    1.11 +         else substring (s', 0, 1)) ^ atom_suffix s m
    1.12        end
    1.13      | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
    1.14      | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])