# HG changeset patch
# User wenzelm
# Date 1207832651 -7200
# Node ID b5fd3ad271ec7a0b441cc9d653effbd7bc903da2
# Parent  8a9d3eebd5344e3419234ae5ed95f5bbd4c95f8b
eliminated backpatching of load_thy;

diff -r 8a9d3eebd534 -r b5fd3ad271ec src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Apr 10 14:53:31 2008 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Apr 10 15:04:11 2008 +0200
@@ -28,17 +28,9 @@
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
-  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
 end;
 
-signature PRIVATE_THY_LOAD =
-sig
-  include THY_LOAD
-  (*this backdoor is sealed later*)
-  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> unit) ref
-end;
-
-structure ThyLoad: PRIVATE_THY_LOAD =
+structure ThyLoad: THY_LOAD =
 struct
 
 
@@ -121,11 +113,6 @@
     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
   | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
 
-(*dependent on outer syntax*)
-val load_thy_fn =
-  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> unit);
-fun load_thy dir name pos text time = ! load_thy_fn dir name pos text time;
-
 end;
 
 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;