diff -r 717e96cf9527 -r 7270ae921cf2 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -118,7 +118,7 @@
     val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
 
     val str0 = string_of_int o the_default 0
-    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
+    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos)
     val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
   in
     only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)