diff -r be8234f37e48 -r a0e9501d56f8 src/Pure/Syntax/printer.ML
--- 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);