diff -r 27af754f50ca -r f22054b192b0 src/Pure/ROOT --- a/src/Pure/ROOT Tue Nov 10 20:49:48 2015 +0100 +++ b/src/Pure/ROOT Tue Nov 10 21:31:14 2015 +0100 @@ -227,6 +227,7 @@ "System/message_channel.ML" "System/options.ML" "System/system_channel.ML" + "Thy/document_antiquotations.ML" "Thy/html.ML" "Thy/latex.ML" "Thy/markdown.ML"