Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed call of store_thm_db so that it's result is not displayed
authorclasohm
Thu, 22 Jun 1995 12:58:39 +0200
changeset 1154 bc295e3dc078
parent 1153 5c5daf97cf2d
child 1155 928a16e02f9f
changed call of store_thm_db so that it's result is not displayed by PolyML or SML
src/Pure/Thy/thy_read.ML file | annotate | diff | comparison | revisions 
--- 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*)
isabelle