1.1 --- a/src/Pure/Thy/present.ML	Mon Aug 23 18:33:55 2004 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Aug 23 18:35:11 2004 +0200
     1.3 @@ -24,7 +24,8 @@
     1.4    val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
     1.5    val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
     1.6    val theory_output: string -> string -> unit
     1.7 -  val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
     1.8 +  val begin_theory: Path.T option -> string -> string list ->
     1.9 +    (Path.T * bool) list -> theory -> theory
    1.10    val add_hook: (string -> (string * thm list) list -> unit) -> unit
    1.11    val results: string -> (string * thm list) list -> unit
    1.12    val theorem: string -> thm -> unit
    1.13 @@ -432,16 +433,16 @@
    1.14         (html_path name))), name)
    1.15    end;
    1.16  
    1.17 -fun begin_theory name raw_parents orig_files thy =
    1.18 +fun begin_theory optpath name raw_parents orig_files thy =
    1.19      with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
    1.20    let
    1.21      val parents = map (parent_link remote_path path) raw_parents;
    1.22      val ml_path = ThyLoad.ml_path name;
    1.23      val files = map (apsnd Some) orig_files @
    1.24 -      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []);
    1.25 +      (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, None)] else []);
    1.26  
    1.27      fun prep_file (raw_path, loadit) =
    1.28 -      (case ThyLoad.check_file raw_path of
    1.29 +      (case ThyLoad.check_file optpath raw_path of
    1.30          Some (path, _) =>
    1.31            let
    1.32              val base = Path.base path;