--- a/src/Pure/ROOT.ML Fri Jan 29 17:08:20 1999 +0100
+++ b/src/Pure/ROOT.ML Fri Jan 29 17:10:26 1999 +0100
@@ -11,6 +11,11 @@
print_depth 1;
+(* global flags *)
+val print_mode = ref ([]:string list);
+(*if true then some packages will OMIT SOME PROOFS*)
+val quick_and_dirty = ref false;
+
(*fake hiding of private structures*)
structure Hidden = struct end;
@@ -63,9 +68,6 @@
use "install_pp.ML";
-(*if true then some packages will OMIT SOME PROOFS*)
-val quick_and_dirty = ref false;
-
(*several object-logics declare theories that hide basis library structures*)
structure BasisLibrary =
struct
--- a/src/Pure/Syntax/printer.ML Fri Jan 29 17:08:20 1999 +0100
+++ b/src/Pure/Syntax/printer.ML Fri Jan 29 17:10:26 1999 +0100
@@ -11,7 +11,6 @@
val show_sorts: bool ref
val show_types: bool ref
val show_no_free_types: bool ref
- val print_mode: string list ref
end;
signature PRINTER =
@@ -42,7 +41,6 @@
val show_sorts = ref false;
val show_brackets = ref false;
val show_no_free_types = ref false;
-val print_mode = ref ([]:string list);