# HG changeset patch
# User wenzelm
# Date 918491583 -3600
# Node ID 87e5f5b4059547828a3afb8b1b1a6d3c9a4732ba
# Parent  f30d1e31b9df8ff6bd435c3b16c557f47ebb74e9
use: provide context;

diff -r f30d1e31b9df -r 87e5f5b40595 src/Pure/Isar/isar_cmd.ML
--- 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;