| changeset 51556 | 7ada6dfa9ab5 |
| parent 51267 | c68c1b89a0f1 |
| child 51626 | e09446d3caca |
--- a/src/Pure/Thy/thy_output.ML Wed Mar 27 17:53:29 2013 +0100 +++ b/src/Pure/Thy/thy_output.ML Wed Mar 27 17:55:21 2013 +0100 @@ -206,7 +206,8 @@ fun check_text (txt, pos) state = (Position.report pos Markup.doc_source; - ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); + if Toplevel.is_skipped_proof state then () + else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));