diff -r 7f35355df72e -r 0cf166548856 Quot/ROOT.ML
--- a/Quot/ROOT.ML	Mon Dec 07 15:18:44 2009 +0100
+++ b/Quot/ROOT.ML	Mon Dec 07 15:21:51 2009 +0100
@@ -1,8 +1,9 @@
-no_document use_thys 
+quick_and_dirty := true;
+
+no_document use_thys
    ["QuotMain",
     "Examples/Fset",
     "Examples/IntEx",
     "Examples/IntEx2",
     "Examples/LFex",
     "Examples/LamEx"];
-