# HG changeset patch
# User wenzelm
# Date 933105519 -7200
# Node ID 1c44df10a7bc538f98a774258c94b89c60212ffe
# Parent  ead5c234b28c2ea375dd1d5544e572b3b945e18c
removed update_context;
context / theory: proper update in interactive mode;

diff -r ead5c234b28c -r 1c44df10a7bc src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Jul 27 21:57:58 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Jul 27 21:58:39 1999 +0200
@@ -147,7 +147,6 @@
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
   val context: string -> Toplevel.transition -> Toplevel.transition
-  val update_context: string -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure IsarThy: ISAR_THY =
@@ -463,7 +462,11 @@
 
 fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy);
 
-fun bg_theory (name, parents, files) () = begin_theory name parents files;
+
+fun bg_theory (name, parents, files) int =
+  (if int then seq ThyInfo.update_thy parents else ();   (*FIXME robust!? *)
+    begin_theory name parents files);
+
 fun en_theory thy = (end_theory thy; ());
 
 fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory kill_theory;
@@ -471,11 +474,9 @@
 
 (* context switch *)
 
-fun switch_theory load s =
-  Toplevel.init_theory (fn () => (the (#2 (Context.pass None load s)))) (K ()) (K ());
-
-val context = switch_theory ThyInfo.use_thy;
-val update_context = switch_theory ThyInfo.update_thy;
+fun context name =
+  Toplevel.init_theory (fn _ => (the (#2 (Context.pass None ThyInfo.update_thy name))))
+  (K ()) (K ());
 
 
 end;