theory Foo imports Bar begin

 ML {*

   @{theory Bar};           (*OK                                                     *)

 (*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)

   case Thy_Info.lookup_theory "Bar" of

     NONE => writeln "Expected, if Foo.thy is loaded directly. "

   | SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar."

 *}

 end