# HG changeset patch
# User wenzelm
# Date 964715101 -7200
# Node ID 5c25ed3c10a0efcc243f5cb1cf422f6f944d0376
# Parent  c97dba47e5041c1ac7ff8896c5bb4c31732cdde0
begin_theory: store *copy* of initial theory;

diff -r c97dba47e504 -r 5c25ed3c10a0 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jul 27 18:23:12 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 27 18:25:01 2000 +0200
@@ -383,10 +383,13 @@
     val deps =
       if known_thy name then get_deps name
       else (init_deps None (map #1 paths));   (*records additional ML files only!*)
-    val _ = change_thys (update_node name parents (deps, Some theory));
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
+
+    val _ = change_thys (update_node name parents (deps, Some (Theory.copy theory)));
     val theory' = theory |> present name parents paths;
+    val _ = put_theory name (Theory.copy theory');
     val ((), theory'') = Context.pass_theory theory' (seq (load_file false)) use_paths;
+    val _ = put_theory name (Theory.copy theory'');
   in theory'' end;
 
 fun end_theory theory =