# HG changeset patch
# User wenzelm
# Date 1492766519 -7200
# Node ID 53fd6cf53ec2b07205122a7b878ffa89bafb08ef
# Parent  d15d302da7f03f1a6f01436f498139a899648e36
tuned;

diff -r d15d302da7f0 -r 53fd6cf53ec2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Apr 21 10:59:07 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Apr 21 11:21:59 2017 +0200
@@ -93,8 +93,8 @@
         }
     }
 
-  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
-    import_name(theory_qualifier(node_name), node_name.master_dir, s)
+  def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
+    import_name(theory_qualifier(name), name.master_dir, s)
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {