src/Pure/Isar/toplevel.ML

   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: string -> (bool -> theory) -> transition -> transition
+  val init_theory: string -> (unit -> theory) -> transition -> transition
+  val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
   val ignored: Position.T -> transition

 
 
 (* primitive transitions *)
 
 datatype trans =
-  Init of string * (bool -> theory) |    (*theory name, init*)
+  Init of string * (unit -> theory) |    (*theory name, init*)
   Exit |                                 (*formal exit of theory*)
   Keep of bool -> state -> unit |        (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
-fun apply_tr int (Init (_, f)) (State (NONE, _)) =
+fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
-          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
+          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
       State (NONE, prev)
   | apply_tr int (Keep f) state =
       Runtime.controlled_execution (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =

 
 
 (* basic transitions *)
 
 fun init_theory name f = add_trans (Init (name, f));
+
+fun modify_init f tr =
+  (case init_of tr of
+    SOME name => init_theory name f (reset_trans tr)
+  | NONE => tr);
+
 val exit = add_trans Exit;
 val keep' = add_trans o Keep;
 
 fun present_transaction f g = add_trans (Transaction (f, g));
 fun transaction f = present_transaction f (K ());