--- a/src/Pure/Thy/thy_header.ML Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Aug 17 19:34:15 2015 +0200
@@ -78,7 +78,9 @@
((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
- (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
+ (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
+ (("ML_file_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
+ (("ML_file_no_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
(* theory data *)