Adapted use command to new behaviour of Toplevel.node_trans

--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 21 19:13:03 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 21 19:16:19 2005 +0200
@@ -155,8 +155,8 @@
 
 (* use ML text *)
 
-fun use path = Toplevel.keep (fn state =>
-  Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
+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));
 
 (*passes changes of theory context*)
 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;