--- a/src/Pure/General/secure.ML Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Pure/General/secure.ML Tue Jun 01 13:32:05 2010 +0200
@@ -13,7 +13,8 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
- val open_unsynchronized: unit -> unit
+ val Isar_setup: unit -> unit
+ val PG_setup: unit -> unit
val commit: unit -> unit
val bash_output: string -> string * int
val bash: string -> int
@@ -54,7 +55,9 @@
val use_global = raw_use_text ML_Parse.global_context (0, "") false;
fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-fun open_unsynchronized () = use_global "open Unsynchronized";
+
+fun Isar_setup () = use_global "open Unsynchronized;";
+fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
(* shell commands *)