clarified default position for empty message pos;

--- a/src/Pure/General/position.ML	Mon Dec 25 11:22:49 2017 +0100
+++ b/src/Pure/General/position.ML	Wed Dec 27 11:51:38 2017 +0100
@@ -24,6 +24,7 @@
   val line_file_only: int -> string -> T
   val line_file: int -> string -> T
   val line: int -> T
+  val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
   val get_id: T -> string option
@@ -131,6 +132,8 @@
 fun line_file i name = Pos ((i, 1, 0), file_name name);
 fun line i = line_file i "";
 
+fun get_props (Pos (_, props)) = props;
+
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 

--- a/src/Pure/Thy/bibtex.ML	Mon Dec 25 11:22:49 2017 +0100
+++ b/src/Pure/Thy/bibtex.ML	Wed Dec 27 11:51:38 2017 +0100
@@ -24,8 +24,7 @@
   |> YXML.parse_body
   |> let open XML.Decode in list (triple bool string properties) end
   |> map (fn (is_error, msg, pos) =>
-      {is_error = is_error, msg = msg,
-        pos = Position.of_properties (pos @ Position.properties_of pos0)});
+      {is_error = is_error, msg = msg, pos = Position.of_properties (pos @ Position.get_props pos0)});
 
 fun check_database_output pos0 database =
   let