--- 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)]};
--- 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