src/Pure/Isar/toplevel.ML

   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
   val interact: bool Unsynchronized.ref
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
-  val debug: bool Unsynchronized.ref
-  val debugging: ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: ('a -> 'b) -> 'a -> 'b
+  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val program: (unit -> 'a) -> 'a
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
   val print_of: transition -> bool

 val profiling = Unsynchronized.ref 0;
 
 
 (* controlled execution *)
 
-val debug = Runtime.debug;
-fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
-fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
+fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
+fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
 
 fun program body =
  (body
-  |> controlled_execution
+  |> controlled_execution NONE
   |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
 
 fun thread interrupts body =
   Thread.fork
     (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
-        |> debugging
+        |> debugging NONE
         |> Runtime.toplevel_error
           (fn exn =>
             Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
       Simple_Thread.attributes interrupts);
 

 in
 
 fun apply_transaction f g node =
   let
     val cont_node = reset_presentation node;
+    val context = cases_node I (Context.Proof o Proof.context_of) cont_node;
     fun state_error e nd = (State (SOME nd, SOME node), e);
 
     val (result, err) =
       cont_node
-      |> controlled_execution f
+      |> controlled_execution (SOME context) f
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
   in
     (case err of
       NONE => tap g result

   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
 fun apply_tr _ (Init f) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
+      State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
       exit_transaction state
   | apply_tr int (Keep f) state =
-      controlled_execution (fn x => tap (f int) x) state
+      controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
       apply_transaction (fn x => f int x) g state
   | apply_tr _ _ _ = raise UNDEF;
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)