author | Walther Neuper <neuper@ist.tugraz.at> |
Fri, 13 Sep 2013 18:57:11 +0200 | |
changeset 52102 | cd5494eb08fd |
child 59472 | 3e904f8ec16c |
permissions | -rw-r--r-- |
1 theory Foo imports Bar begin
2 ML {*
3 @{theory Bar}; (*OK *)
4 (*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)
5 case Thy_Info.lookup_theory "Bar" of
6 NONE => writeln "Expected, if Foo.thy is loaded directly. "
7 | SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar."
8 *}
9 end