# HG changeset patch
# User wenzelm
# Date 1003870388 -7200
# Node ID 8b8923bfc25991e127d35342c390094f48efade7
# Parent  92e442b783db4ad6cdd5a28133c46d905ec048da
build option;

diff -r 92e442b783db -r 8b8923bfc259 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Oct 23 22:52:45 2001 +0200
+++ b/src/Pure/Isar/session.ML	Tue Oct 23 22:53:08 2001 +0200
@@ -10,7 +10,7 @@
 sig
   val name: unit -> string
   val welcome: unit -> string
-  val use_dir: string list -> bool -> bool -> string -> bool -> string
+  val use_dir: bool -> string list -> bool -> bool -> string -> bool -> string
     -> string -> string -> string -> int -> bool -> unit
   val finish: unit -> unit
 end;
@@ -78,11 +78,11 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir modes reset info doc doc_graph parent name dump rpath_str level verbose =
+fun use_dir build modes reset info doc doc_graph parent name dump rpath_str level verbose =
   Library.setmp print_mode (modes @ ! print_mode)
     (Library.setmp Proofterm.proofs level (fn () =>
       (init reset parent name;
-       Present.init info doc doc_graph (path ()) name
+       Present.init build info doc doc_graph (path ()) name
          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
        File.symbol_use root_file;
        finish ()))) ()