changeset 68506 | cef6c6b009fb |
parent 68491 | f0f83ce0badd |
child 68839 | d8251a61cce8 |
--- a/src/Pure/Thy/thy_info.ML Tue Jun 26 14:01:46 2018 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Jun 26 14:39:49 2018 +0200 @@ -56,7 +56,7 @@ if exists (Toplevel.is_skipped_proof o #state) segments then () else let - val body = Thy_Output.present_thy thy segments; + val body = Thy_Output.present_thy options thy segments; val option = Present.document_option options; in if #disabled option then ()