Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
leave theory context after load_thy;
authorwenzelm
Thu, 04 Feb 1999 18:16:22 +0100
changeset 6229 f839b261b87f
parent 6228 64f18b89d5d5
child 6230 85fc589a66ea
leave theory context after load_thy;
src/Pure/Isar/outer_syntax.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle