# HG changeset patch
# User wenzelm
# Date 1492781184 -7200
# Node ID b6250ee6ce79912b754da4a61654eaea86054e6d
# Parent  4a7e794944df5b5eaae5cc8dce5e7a7fa020f69d
clarified local_theories: exclude ancestor sessions;

diff -r 4a7e794944df -r b6250ee6ce79 src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 15:00:31 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 15:26:24 2017 +0200
@@ -69,7 +69,11 @@
       val info = full_sessions(session_name)
       val session_base = deps(session_name)
       val resources = new Resources(session_base)
-      val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
+      val local_theories =
+        (for {
+          (_, name) <- session_base.known.theories_local.iterator
+          if resources.theory_qualifier(name) == info.theory_qualifier
+        } yield name).toSet
 
       def standard_import(qualifier: String, dir: String, s: String): String =
       {