# HG changeset patch
# User wenzelm
# Date 953574467 -3600
# Node ID e8ab6cd2e9083e2abfa8d68639879694e2fb5985
# Parent  8abfc72109f2a26e31e6a3bf864e09d00cef683f
quick_and_dirty moved to Isar/skip_proof.ML;

diff -r 8abfc72109f2 -r e8ab6cd2e908 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Mar 20 18:47:27 2000 +0100
+++ b/src/Pure/ROOT.ML	Mon Mar 20 18:47:47 2000 +0100
@@ -13,7 +13,6 @@
 
 (*global flags*)
 val print_mode = ref ([]: string list);
-val quick_and_dirty = ref false;        (*if true then some packages will OMIT SOME PROOFS*)
 
 (*fake hiding of private structures*)
 structure Hidden = struct end;