show strings as "s_1" etc. rather than "l_1" etc.
authorblanchet
Mon Dec 06 14:47:58 2010 +0100 (2010-12-06)
changeset 41039405a9f41ad6b
parent 41038 9592334001d5
child 41040 a4a5a465da8d
show strings as "s_1" etc. rather than "l_1" etc.
src/HOL/Tools/Nitpick/nitpick_model.ML
     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], [])