src/Pure/pure_syn.ML
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"