# HG changeset patch
# User wenzelm
# Date 1218569285 -7200
# Node ID 0bd68bf0cbb86c90d8c82b723c0fcb5aa24a2beb
# Parent  6c35d50d309f162692242fae889af36013842246
load_thy: removed obsolete dir argument;

diff -r 6c35d50d309f -r 0bd68bf0cbb8 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 12 21:28:03 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 12 21:28:05 2008 +0200
@@ -288,7 +288,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy time upd_time initiators dir name =
+fun load_thy time upd_time initiators name =
   let
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
     val (pos, text, files) =
@@ -300,7 +300,7 @@
     val _ = CRITICAL (fn () =>
       change_deps name (Option.map (fn {master, text, parents, files, ...} =>
         make_deps upd_time master text parents files)));
-    val _ = OuterSyntax.load_thy dir name pos text (time orelse ! Output.timing);
+    val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
   in
     CRITICAL (fn () =>
      (change_deps name
@@ -435,7 +435,7 @@
           val upd_time = serial ();
           val tasks_graph'' = tasks_graph' |> new_deps name parent_names
            (if all_current then Finished
-            else Task (fn () => load_thy time upd_time initiators dir' name));
+            else Task (fn () => load_thy time upd_time initiators name));
           val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
         in (all_current, (tasks_graph'', tasks_len'')) end)
   end;