--- a/src/Pure/Thy/thy_read.ML Thu Apr 11 08:30:25 1996 +0200
+++ b/src/Pure/Thy/thy_read.ML Thu Apr 11 13:41:22 1996 +0200
@@ -577,11 +577,11 @@
(*Invoke every put method stored in a theory's methods table to initialize
the state of user defined variables*)
-fun set_current_thy tname =
+fun put_thydata first tname =
let val (methods, data) =
case get_thyinfo tname of
Some (ThyInfo {methods, data, ...}) =>
- (methods, Symtab.dest (fst data))
+ (methods, Symtab.dest ((if first then fst else snd) data))
| None => error ("Theory " ^ tname ^ " not stored by loader");
fun put_data (id, date) =
@@ -591,6 +591,8 @@
id ^ "\"");
in seq put_data data end;
+val set_current_thy = put_thydata false;
+
(*Read .thy and .ML files that haven't been read yet or have changed since
they were last read;
loaded_thys is a thy_info list ref containing all theories that have
@@ -723,7 +725,7 @@
in if thy_uptodate andalso ml_uptodate then ()
else
(if thy_file = "" then ()
- else if thy_uptodate then set_current_thy tname
+ else if thy_uptodate then put_thydata true tname
else
(writeln ("Reading \"" ^ name ^ ".thy\"");