use: provide context;

--- 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;