author | blanchet |
Wed, 20 Jul 2011 00:37:42 +0200 | |
changeset 43904 | 95d8a2f2bffe |
parent 43903 | 1e2aa420c660 |
child 43905 | 1ace987e22e5 |
--- 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