# HG changeset patch
# User wenzelm
# Date 934814664 -7200
# Node ID 8e4aa9044599ac08448f5ca05f6761cd473e8a33
# Parent  ae9a645e8728d3f100890da4bf98f205ea56ae72
fixed thy_only;

diff -r ae9a645e8728 -r 8e4aa9044599 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Aug 16 15:15:14 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Aug 16 16:44:24 1999 +0200
@@ -96,6 +96,9 @@
 fun make_deps present outdated master files =
   {present = present, outdated = outdated, master = master, files = files}: deps;
 
+fun init_deps master files = Some (make_deps false true master (map (rpair None) files));
+
+
 type thy = deps option * theory option;
 
 local
@@ -253,7 +256,7 @@
 
 (* require_thy *)
 
-fun init_deps master files = Some (make_deps false true master (map (rpair None) files));
+local
 
 fun load_deps dir name =
   let val (master, (parents, files)) = ThyLoad.deps_thy dir name
@@ -288,7 +291,7 @@
       let
         val dir = Path.append prfx (Path.dir path);
         val req_parent =
-          require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
+          require_thy true time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
 
         val (current, (new_deps, parents)) = current_deps strict dir name handle ERROR =>
           error (loader_msg "the error(s) above occurred while examining theory" [name] ^
@@ -310,6 +313,8 @@
   let val (_, (_, name)) = req [] Path.current ([], s)
   in Context.context (get_theory name) end;
 
+in
+
 val weak_use_thy    = gen_use_thy (require_thy true false false false);
 val use_thy         = gen_use_thy (require_thy true false true false);
 val time_use_thy    = gen_use_thy (require_thy true true true false);
@@ -317,6 +322,8 @@
 val update_thy      = gen_use_thy (require_thy true false true true);
 val update_thy_only = gen_use_thy (require_thy false false true true);
 
+end;
+
 
 (* remove_thy *)