author | wenzelm |
Mon, 08 Feb 1999 17:33:03 +0100 | |
changeset 6264 | 87e5f5b40595 |
parent 6263 | f30d1e31b9df |
child 6265 | aaabe48bafcb |
--- 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;