# HG changeset patch
# User wenzelm
# Date 1496919295 -7200
# Node ID 58d2e41afbfe5b00a51e6ef2caad35583c0801dd
# Parent  b6396880b64417c95124560f8d63fc4b8ed1be69
more official session qualifier;

diff -r b6396880b644 -r 58d2e41afbfe src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jun 08 12:25:59 2017 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jun 08 12:54:55 2017 +0200
@@ -6,7 +6,7 @@
 
 signature PRESENT =
 sig
-  val session_name: theory -> string
+  val theory_qualifier: theory -> string
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -51,8 +51,6 @@
 val _ = Theory.setup
   (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
 
-val session_name = #name o Browser_Info.get;
-
 
 
 (** global browser info state **)
@@ -133,10 +131,12 @@
 
 fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
 
+val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;
+
 fun is_session_theory thy =
   (case ! session_info of
     NONE => false
-  | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy));
+  | SOME {name, ...} => name = theory_qualifier thy);
 
 
 (** document preparation **)
diff -r b6396880b644 -r 58d2e41afbfe src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Jun 08 12:25:59 2017 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Jun 08 12:54:55 2017 +0200
@@ -29,7 +29,7 @@
                 a :: _ =>
                   (case try (Context.get_theory thy) a of
                     SOME thy =>
-                      (case Present.session_name thy of
+                      (case Present.theory_qualifier thy of
                         "" => []
                       | session => [session])
                   | NONE => [])