src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
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