# HG changeset patch
# User wenzelm
# Date 1116852995 -7200
# Node ID 6e2c020eed45bade71584a8f54334199d90ca344
# Parent  6887e6d12a94fa0b41b7fbf7e2c969a3df868353
use: not a theory command!

diff -r 6887e6d12a94 -r 6e2c020eed45 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon May 23 13:39:45 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon May 23 14:56:35 2005 +0200
@@ -156,8 +156,8 @@
 
 (* use ML text *)
 
-fun use path = Toplevel.keep (fn state => ThyInfo.load_file false path) o
-  Toplevel.theory (fn thy => (Context.setmp (SOME thy) (ThyInfo.load_file false) path; thy));
+fun use path = Toplevel.keep (fn state =>
+  Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
 
 (*passes changes of theory context*)
 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;