# HG changeset patch
# User wenzelm
# Date 896124487 -7200
# Node ID 47b8f2d12c53381030ff83f1e051339f6128e771
# Parent  06914837e073de063bb05eae5c441381ef1e54f4
tuned store_theory;

diff -r 06914837e073 -r 47b8f2d12c53 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Mon May 25 21:27:22 1998 +0200
+++ b/src/Pure/Thy/thy_read.ML	Mon May 25 21:28:07 1998 +0200
@@ -267,8 +267,7 @@
              Use.use ml_file);
 
        (*Store theory again because it could have been redefined*)
-       use_strings
-         ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
+       use_strings ["val _ = store_theory " ^ tname ^ ".thy;"];
 
        (*Add theory to list of all loaded theories (for index.html)
          and add it to its parents' sub-charts*)