src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -46,7 +46,8 @@
   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
@@ -295,16 +296,16 @@
 (* 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 =
@@ -394,6 +395,12 @@
 (* 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;