# HG changeset patch
# User wenzelm
# Date 1185201904 -7200
# Node ID 66923825628e9fce86aeef6b2c887476d44d8112
# Parent  2a4e42ec9a543258f172da9bb10edee821caa98f
setmp_noncritical (assumes outermost control);

diff -r 2a4e42ec9a54 -r 66923825628e src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Mon Jul 23 16:45:03 2007 +0200
+++ b/src/Pure/Isar/session.ML	Mon Jul 23 16:45:04 2007 +0200
@@ -80,8 +80,8 @@
 
 fun use_dir root build modes reset info doc doc_graph doc_versions
     parent name dump rpath level verbose =
-  Library.setmp print_mode (modes @ ! print_mode)
-    (Library.setmp Proofterm.proofs level (fn () =>
+  setmp_noncritical print_mode (modes @ ! print_mode)
+    (setmp_noncritical Proofterm.proofs level (fn () =>
       (init reset parent name;
        Present.init build info doc doc_graph doc_versions (path ()) name
          (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));