proper range position;

--- a/src/Pure/Isar/proof.ML	Wed Jan 16 16:26:36 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 16 18:43:59 2013 +0100
@@ -827,7 +827,8 @@
     val (finish_text, terminal_pos, finished_pos) =
       (case opt_text of
         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
-      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
+      | SOME (text, (pos, end_pos)) =>
+          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
   in
     Seq.APPEND (fn state =>
       state