# HG changeset patch
# User wenzelm
# Date 899210487 -7200
# Node ID f616efb64a0e1dea653d75a817e3c5df4f20418b
# Parent  e443bc494604c17aadc27273811f5ac48a4b829a
added quick_and_dirty flag;

diff -r e443bc494604 -r f616efb64a0e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 29 21:33:35 1998 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 30 14:41:27 1998 +0200
@@ -55,6 +55,8 @@
 
 use "install_pp.ML";
 
+val quick_and_dirty = ref false;
+
 (*several object-logics declare theories named List or Option, hiding
   the eponymous basis library structures*)
 structure BasisLibrary =