# HG changeset patch
# User wenzelm
# Date 1313261381 -7200
# Node ID 88d770052bacf2a8d0aa49ae9b6fc873d09851e9
# Parent  806f0ec1a43dbc086763965aeca01635ca97c312
simplified Toplevel.init_theory: discontinued special name argument;

diff -r 806f0ec1a43d -r 88d770052bac src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:41:29 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:49:41 2011 +0200
@@ -30,7 +30,7 @@
   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     (Thy_Header.args >> (fn (name, imports, uses) =>
       Toplevel.print o
-        Toplevel.init_theory name
+        Toplevel.init_theory
           (fn () =>
             Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
               name imports (map (apfst Path.explode) uses))));
diff -r 806f0ec1a43d -r 88d770052bac src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:41:29 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:49:41 2011 +0200
@@ -224,7 +224,7 @@
 fun process_file path thy =
   let
     val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
+    val init = Toplevel.init_theory (K thy) Toplevel.empty;
     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   in
     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
diff -r 806f0ec1a43d -r 88d770052bac src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:41:29 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:49:41 2011 +0200
@@ -34,7 +34,6 @@
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
-  val is_init: transition -> bool
   val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
@@ -45,7 +44,8 @@
   val set_print: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: string -> (unit -> theory) -> transition -> transition
+  val init_theory: (unit -> theory) -> transition -> transition
+  val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
@@ -296,14 +296,14 @@
 (* primitive transitions *)
 
 datatype trans =
-  Init of string * (unit -> theory) | (*theory name, init*)
+  Init of unit -> theory |               (*init theory*)
   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 _ (Init (_, f)) (State (NONE, _)) =
+fun apply_tr _ (Init f) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
           (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
@@ -352,11 +352,6 @@
 
 (* diagnostics *)
 
-fun get_init (Transition {trans = [Init args], ...}) = SOME args
-  | get_init _ = NONE;
-
-val is_init = is_some o get_init;
-
 fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
@@ -397,12 +392,12 @@
 
 (* basic transitions *)
 
-fun init_theory name f = add_trans (Init (name, f));
+fun init_theory f = add_trans (Init f);
 
-fun modify_init f tr =
-  (case get_init tr of
-    SOME (name, _) => init_theory name f (reset_trans tr)
-  | NONE => tr);
+fun is_init (Transition {trans = [Init _], ...}) = true
+  | is_init _ = false;
+
+fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr;
 
 val exit = add_trans Exit;
 val keep' = add_trans o Keep;