# HG changeset patch
# User wenzelm
# Date 1207832007 -7200
# Node ID 03455add48012cdf038e4d792a96cd29fb14ef4e
# Parent  df8c1ffdb8cce3a021b87de8b433a189bd17497a
export load_thy -- no backpatching;

diff -r df8c1ffdb8cc -r 03455add4801 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 10 14:53:26 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 10 14:53:27 2008 +0200
@@ -29,6 +29,7 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: bool -> isar
+  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =
@@ -275,9 +276,7 @@
 fun check_text s state = (ThyOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
 
 
-(* load_thy (backpatching) *)
-
-local
+(* load_thy *)
 
 fun load_thy dir name pos text time =
   let
@@ -301,9 +300,5 @@
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   in () end;
 
-in val _ = ThyLoad.load_thy_fn := load_thy end;
-
 end;
 
-structure ThyLoad: THY_LOAD = ThyLoad;
-