src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/ROOT.ML	Fri May 17 20:41:45 2013 +0200
@@ -6,9 +6,6 @@
   val is_official = false;
 end;
 
-(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = Unsynchronized.ref false;
-
 print_depth 10;
 
 
@@ -118,6 +115,9 @@
 use "context_position.ML";
 use "config.ML";
 
+val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
 
 (* inner syntax *)