diff -r 717e96cf9527 -r 7270ae921cf2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -64,8 +64,8 @@
   let
     fun do_line line =
       case line |> space_explode ":" of
-        [line_num, col_num, proof] =>
-        SOME (pairself (the o Int.fromString) (line_num, col_num),
+        [line_num, offset, proof] =>
+        SOME (pairself (the o Int.fromString) (line_num, offset),
               proof |> space_explode " " |> filter_out (curry (op =) ""))
        | _ => NONE
     val proofs = File.read (Path.explode proof_file)
@@ -105,9 +105,9 @@
 fun with_index (i, s) = s ^ "@" ^ string_of_int i
 
 fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) =
-  case (Position.line_of pos, Position.column_of pos) of
-    (SOME line_num, SOME col_num) =>
-    (case Prooftab.lookup (!proof_table) (line_num, col_num) of
+  case (Position.line_of pos, Position.offset_of pos) of
+    (SOME line_num, SOME offset) =>
+    (case Prooftab.lookup (!proof_table) (line_num, offset) of
        SOME proofs =>
        let
          val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre