# HG changeset patch
# User wenzelm
# Date 918148582 -3600
# Node ID f839b261b87f9f93b884fa13d7ee41ad9ab6d4f5
# Parent  64f18b89d5d52717130d83bfb72fd6fd7b42637a
leave theory context after load_thy;

diff -r 64f18b89d5d5 -r f839b261b87f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Feb 04 18:15:53 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Feb 04 18:16:22 1999 +0100
@@ -214,8 +214,7 @@
       if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
       else (Toplevel.excursion (parse_thy (src, pos))
         handle exn => error (Toplevel.exn_message exn));
-    val theory = ThyInfo.get_theory name;
-  in Context.setmp theory try_ml_file name ml end;
+  in Context.context (ThyInfo.get_theory name); try_ml_file name ml end;
 
 fun load_thy name ml time path =
   if not time then read_thy name ml path