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

     2.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Oct 28 13:55:17 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 28 14:00:25 1999 +0200
     2.3 @@ -158,7 +158,7 @@
     2.4    val kill_theory: string -> unit
     2.5    val theory: string * string list * (string * bool) list
     2.6      -> Toplevel.transition -> Toplevel.transition
     2.7 -  val init_context: (string -> unit) -> string -> Toplevel.transition -> Toplevel.transition
     2.8 +  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
     2.9    val context: string -> Toplevel.transition -> Toplevel.transition
    2.10  end;
    2.11  
    2.12 @@ -537,8 +537,12 @@
    2.13  
    2.14  (* context switch *)
    2.15  
    2.16 -fun init_context (f: string -> unit) name =
    2.17 -  Toplevel.init_theory (fn _ => (the (#2 (Context.pass None f name)))) (K ()) (K ());
    2.18 +fun fetch_context f x =
    2.19 +  (case Context.pass None f x of
    2.20 +    ((), None) => raise Toplevel.UNDEF
    2.21 +  | ((), Some thy) => thy);
    2.22 +
    2.23 +fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());
    2.24  
    2.25  val context = init_context (ThyInfo.quiet_update_thy true);
    2.26