# HG changeset patch
# User wenzelm
# Date 1514467248 -3600
# Node ID bef14fa789ef569098021cd970296b5f4b30ca58
# Parent  aa9d28034945dcd51ed0ec105fcffbc4ce85e53b
clarified signature: prefer Document.Node.Name.is_bibtex;

diff -r aa9d28034945 -r bef14fa789ef src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu Dec 28 12:44:42 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Dec 28 14:20:48 2017 +0100
@@ -130,7 +130,6 @@
   /** document model **/
 
   def check_name(name: String): Boolean = name.endsWith(".bib")
-  def check_name(name: Document.Node.Name): Boolean = check_name(name.node)
 
   def entries(text: String): List[Text.Info[String]] =
   {