src/Pure/ML-Systems/ml_positions.ML
changeset 56437 b14bd153a753
parent 56435 28b34e8e4a80
--- a/src/Pure/ML-Systems/ml_positions.ML	Sun Apr 06 15:43:45 2014 +0200
+++ b/src/Pure/ML-Systems/ml_positions.ML	Sun Apr 06 15:51:02 2014 +0200
@@ -7,7 +7,7 @@
 fun ml_positions start_line name txt =
   let
     fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
-          let val s = "(Position.line_file " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
           in positions line cs (s :: res) end
       | positions line (c :: cs) res =
           positions (if c = #"\n" then line + 1 else line) cs (str c :: res)