diff -r 387dc978422b -r 2f970c7f722b src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Fri May 17 20:41:45 2013 +0200
@@ -2,7 +2,7 @@
 theory Isar
 imports LaTeXsugar
 begin
-ML{* quick_and_dirty := true *}
+declare [[quick_and_dirty]]
 (*>*)
 text{*
 Apply-scripts are unreadable and hard to maintain. The language of choice