show strings as "s_1" etc. rather than "l_1" etc.
authorblanchet
Mon, 06 Dec 2010 14:47:58 +0100
changeset 41039 405a9f41ad6b
parent 41038 9592334001d5
child 41040 a4a5a465da8d
show strings as "s_1" etc. rather than "l_1" etc.
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], [])