--- a/src/Pure/Thy/bibtex.ML Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML Sun May 24 19:45:42 2020 +0200
@@ -20,7 +20,7 @@
type message = string * Position.T;
fun check_database pos0 database =
- Scala.function "check_bibtex_database" database
+ \<^scala>\<open>check_bibtex_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));