# HG changeset patch
# User wenzelm
# Date 1185909564 -7200
# Node ID 969d334040a8d643dcc805d9f9dd3440bd25118b
# Parent  bdcefe679ced391feef714ea3d814d75fcafbf9e
no_document: setmp_noncritical;

diff -r bdcefe679ced -r 969d334040a8 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Jul 31 21:19:23 2007 +0200
+++ b/src/Pure/Thy/present.ML	Tue Jul 31 21:19:24 2007 +0200
@@ -175,7 +175,7 @@
 fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
 
 val suppress_tex_source = ref false;
-fun no_document f x = Library.setmp suppress_tex_source true f x;
+fun no_document f x = setmp_noncritical suppress_tex_source true f x;
 
 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>