changeset 60189 | 0d3a62127057 |
parent 60096 | 7b98dbc1d13e |
child 61036 | f6f2959bed67 |
--- a/src/Pure/pure_syn.ML Wed Apr 22 18:43:33 2015 +0200 +++ b/src/Pure/pure_syn.ML Wed Apr 22 19:48:32 2015 +0200 @@ -43,7 +43,7 @@ val _ = Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text" - (Parse.document_source >> K (Toplevel.imperative I)); + (Parse.document_source >> K (Toplevel.keep (fn _ => ()))); val _ = Outer_Syntax.command ("theory", @{here}) "begin theory"