# HG changeset patch
# User clasohm
# Date 803818719 -7200
# Node ID bc295e3dc078a814f98dfd23d054e024b81405c9
# Parent  5c5daf97cf2d3cf9954a9a8be7f1ae9434ae2152
changed call of store_thm_db so that it's result is not displayed
by PolyML or SML

diff -r 5c5daf97cf2d -r bc295e3dc078 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Jun 22 12:45:08 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Thu Jun 22 12:58:39 1995 +0200
@@ -285,8 +285,9 @@
          else (writeln ("Reading \"" ^ name ^ ".ML\"");
                use ml_file);
 
-         use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");",
-                     "map store_thm_db (axioms_of " ^ tname ^ ".thy);"];
+         use_string
+           ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
+            \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
                     (*Store theory again because it could have been redefined*)
 
          (*Now set the correct info*)