improved IsarThy.init_context;

--- a/src/Pure/Interface/proof_general.ML	Thu Oct 28 13:55:17 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Thu Oct 28 14:00:25 1999 +0200
@@ -201,7 +201,7 @@
 
 val try_context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
-    (P.name >> IsarThy.init_context try_update_thy_only);
+    (P.name >> (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only));
 
 val restartP =
   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control

--- a/src/Pure/Isar/isar_thy.ML	Thu Oct 28 13:55:17 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 28 14:00:25 1999 +0200
@@ -158,7 +158,7 @@
   val kill_theory: string -> unit
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
-  val init_context: (string -> unit) -> string -> Toplevel.transition -> Toplevel.transition
+  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
   val context: string -> Toplevel.transition -> Toplevel.transition
 end;
 
@@ -537,8 +537,12 @@
 
 (* context switch *)
 
-fun init_context (f: string -> unit) name =
-  Toplevel.init_theory (fn _ => (the (#2 (Context.pass None f name)))) (K ()) (K ());
+fun fetch_context f x =
+  (case Context.pass None f x of
+    ((), None) => raise Toplevel.UNDEF
+  | ((), Some thy) => thy);
+
+fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());
 
 val context = init_context (ThyInfo.quiet_update_thy true);