src/Pure/ROOT.ML
changeset 8538 e8ab6cd2e908
parent 7938 e45599caee6c
child 9959 4a2ae974043d
     1.1 --- a/src/Pure/ROOT.ML	Mon Mar 20 18:47:27 2000 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Mon Mar 20 18:47:47 2000 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4  
     1.5  (*global flags*)
     1.6  val print_mode = ref ([]: string list);
     1.7 -val quick_and_dirty = ref false;        (*if true then some packages will OMIT SOME PROOFS*)
     1.8  
     1.9  (*fake hiding of private structures*)
    1.10  structure Hidden = struct end;