no_document: setmp_noncritical;
authorwenzelm
Tue Jul 31 21:19:24 2007 +0200 (2007-07-31)
changeset 24102969d334040a8
parent 24101 bdcefe679ced
child 24103 c13243a11e37
no_document: setmp_noncritical;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Tue Jul 31 21:19:23 2007 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Jul 31 21:19:24 2007 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
     1.5  
     1.6  val suppress_tex_source = ref false;
     1.7 -fun no_document f x = Library.setmp suppress_tex_source true f x;
     1.8 +fun no_document f x = setmp_noncritical suppress_tex_source true f x;
     1.9  
    1.10  fun init_theory_info name info =
    1.11    change_browser_info (fn (theories, files, tex_index, html_index, graph) =>