changeset 6264 | 87e5f5b40595 |
parent 6243 | fb293dfa2df3 |
child 6635 | f81b9b4c3265 |
--- a/src/Pure/Isar/isar_cmd.ML Mon Feb 08 17:32:24 1999 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Mon Feb 08 17:33:03 1999 +0100 @@ -51,7 +51,8 @@ (* use ML text *) -fun use name = Toplevel.imperative (fn () => ThyInfo.use name); +fun use name = Toplevel.keep (fn state => + Context.setmp (try Toplevel.theory_of state) ThyInfo.use name); (*passes changes of theory context*) val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;