# HG changeset patch
# User wenzelm
# Date 1680360883 -7200
# Node ID 9273eb5d26724fb43c9f4e3b4ba91d1876d58036
# Parent  4b2262cfbf13aeffc9cda9b73267ee049ac26072
tuned signature;

diff -r 4b2262cfbf13 -r 9273eb5d2672 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 15:01:35 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 16:54:43 2023 +0200
@@ -28,7 +28,6 @@
   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 put_id: string -> T -> T
@@ -152,8 +151,6 @@
 fun line_file line name = Pos {line = line, offset = 1, end_offset = 0, props = file_name name};
 fun line line = line_file line "";
 
-val get_props = #props o dest;
-
 fun id id = Pos {line = 0, offset = 1, end_offset = 0, props = [(Markup.idN, id)]};
 fun id_only id = Pos {line = 0, offset = 0, end_offset = 0, props = [(Markup.idN, id)]};
 
diff -r 4b2262cfbf13 -r 9273eb5d2672 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sat Apr 01 15:01:35 2023 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sat Apr 01 16:54:43 2023 +0200
@@ -25,7 +25,8 @@
   \<^scala>\<open>bibtex_check_database\<close> database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
-  |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
+  |> (apply2 o map o apsnd)
+      (fn pos => Position.of_properties (pos @ Position.properties_of pos0));
 
 fun check_database_output pos0 database =
   let val (errors, warnings) = check_database pos0 database in