equal
deleted
inserted
replaced
131 nth ss (m - 1) |
131 nth ss (m - 1) |
132 else case T of |
132 else case T of |
133 Type (s, _) => |
133 Type (s, _) => |
134 let val s' = shortest_name s in |
134 let val s' = shortest_name s in |
135 prefix ^ |
135 prefix ^ |
136 (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^ |
136 (if T = @{typ string} then "s" |
137 atom_suffix s m |
137 else if String.isPrefix "\\" s' then s' |
|
138 else substring (s', 0, 1)) ^ atom_suffix s m |
138 end |
139 end |
139 | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m |
140 | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m |
140 | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) |
141 | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) |
141 end |
142 end |
142 fun nth_atom thy atomss pool for_auto T j = |
143 fun nth_atom thy atomss pool for_auto T j = |