1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ADDTESTS/session-get_theory/Foo.thy	Fri Sep 13 18:57:11 2013 +0200
     1.3 @@ -0,0 +1,9 @@
     1.4 +theory Foo imports Bar begin
     1.5 +ML {*
     1.6 +  @{theory Bar};           (*OK                                                     *)
     1.7 +(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)
     1.8 +  case Thy_Info.lookup_theory "Bar" of
     1.9 +    NONE => writeln "Expected, if Foo.thy is loaded directly. "
    1.10 +  | SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar."
    1.11 +*}
    1.12 +end