src/Pure/ROOT.ML
changeset 52059 2f970c7f722b
parent 52050 b40ed9dcf903
child 52140 88a69da5d3fa
     1.1 --- a/src/Pure/ROOT.ML	Fri May 17 20:30:04 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri May 17 20:41:45 2013 +0200
     1.3 @@ -6,9 +6,6 @@
     1.4    val is_official = false;
     1.5  end;
     1.6  
     1.7 -(*if true then some tools will OMIT some proofs*)
     1.8 -val quick_and_dirty = Unsynchronized.ref false;
     1.9 -
    1.10  print_depth 10;
    1.11  
    1.12  
    1.13 @@ -118,6 +115,9 @@
    1.14  use "context_position.ML";
    1.15  use "config.ML";
    1.16  
    1.17 +val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
    1.18 +val quick_and_dirty = Config.bool quick_and_dirty_raw;
    1.19 +
    1.20  
    1.21  (* inner syntax *)
    1.22