--- a/src/Pure/Thy/bibtex.ML Sat May 23 12:04:24 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML Sat May 23 21:43:30 2020 +0200
@@ -20,7 +20,7 @@
type message = string * Position.T;
fun check_database pos0 database =
- Scala.method "isabelle.Bibtex.check_database_yxml" database
+ Scala.function "check_bibtex_database" 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));