changeset 43904 | 95d8a2f2bffe |
parent 43828 | e07a2c4cbad8 |
child 44089 | 10287833549f |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 19 11:15:38 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 20 00:37:42 2011 +0200 @@ -246,7 +246,7 @@ fun str_of_pos (pos, triv) = let val str0 = string_of_int o the_default 0 in - str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ + str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^ (if triv then "[T]" else "") end