# HG changeset patch # User wenzelm # Date 1189274318 -7200 # Node ID fc3cf01e8af17adc2649a64da3d00336bb64d835 # Parent 7b4aa14d249138c5f34888b47d857e2d21d70d64 Present.session_name; diff -r 7b4aa14d2491 -r fc3cf01e8af1 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sat Sep 08 19:58:37 2007 +0200 +++ b/src/Pure/Thy/thm_deps.ML Sat Sep 08 19:58:38 2007 +0200 @@ -49,7 +49,7 @@ (x :: _) => (case ThyInfo.lookup_theory x of SOME thy => - let val name = #name (Present.get_info thy) + let val name = Present.session_name thy in if name = "" then [] else [name] end | NONE => []) | _ => ["global"]);