fixed bug: cur_thyname was overwritten because of early assignment
authorclasohm
Wed, 06 Dec 1995 14:53:55 +0100
changeset 1386 cf066d9b4c4f
parent 1385 63c3d78df538
child 1387 9bcad9c22fd4
fixed bug: cur_thyname was overwritten because of early assignment
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Dec 01 14:20:09 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Wed Dec 06 14:53:55 1995 +0100
@@ -664,8 +664,7 @@
      end
   in if thy_uptodate andalso ml_uptodate then ()
      else
-      (cur_thyname := tname;
-       if thy_file = "" then ()
+      (if thy_file = "" then ()
        else if thy_uptodate then
          simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname);
                     in the thy_ss end
@@ -694,7 +693,7 @@
           if not (!make_html) then ()
           else thyfile2html abs_path tname
          );
-
+       
        set_info tname (Some (file_info thy_file)) None;
                                        (*mark thy_file as successfully loaded*)
 
@@ -876,7 +875,8 @@
 
       val base_thy = (writeln ("Loading theory " ^ (quote child));
                       merge_thy_list mk_draft (map theory_of mergelist));
- in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
+ in cur_thyname := child;
+    simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
     base_thy
  end;