# HG changeset patch
# User blanchet
# Date 1291643278 -3600
# Node ID 405a9f41ad6bc99baefcc568695292917e607064
# Parent  9592334001d565f54a020ea764d2d74c04bcacb0
show strings as "s_1" etc. rather than "l_1" etc.

diff -r 9592334001d5 -r 405a9f41ad6b src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 06 14:47:58 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 06 14:47:58 2010 +0100
@@ -133,8 +133,9 @@
       Type (s, _) =>
       let val s' = shortest_name s in
         prefix ^
-        (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
-        atom_suffix s m
+        (if T = @{typ string} then "s"
+         else if String.isPrefix "\\" s' then s'
+         else substring (s', 0, 1)) ^ atom_suffix s m
       end
     | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
     | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])