# HG changeset patch
# User blanchet
# Date 1311115062 -7200
# Node ID 95d8a2f2bffe3a8b1b89b8fe09cf95336ae96218
# Parent  1e2aa420c6607e3ae98ea435f53a915b048e21c5
remove offset from Mirabelle output

diff -r 1e2aa420c660 -r 95d8a2f2bffe src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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