treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;

--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 16:09:12 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 16:36:33 2010 +0200
@@ -392,8 +392,7 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_free_types_value #>
-  register_config Syntax.show_question_marks_value #>
+ (register_config Syntax.show_question_marks_value #>
   register_config Goal_Display.show_consts_value #>
   register_config Unify.trace_bound_value #>
   register_config Unify.search_bound_value #>

--- a/src/Pure/Syntax/printer.ML	Fri Sep 03 16:09:12 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 16:36:33 2010 +0200
@@ -9,8 +9,6 @@
   val show_brackets: bool Unsynchronized.ref
   val show_sorts: bool Unsynchronized.ref
   val show_types: bool Unsynchronized.ref
-  val show_free_types_default: bool Unsynchronized.ref
-  val show_free_types_value: Config.value Config.T
   val show_free_types: bool Config.T
   val show_all_types: bool Unsynchronized.ref
   val show_structs: bool Unsynchronized.ref
@@ -56,10 +54,7 @@
 val show_all_types = Unsynchronized.ref false;
 val show_structs = Unsynchronized.ref false;
 
-val show_free_types_default = Unsynchronized.ref true;
-val show_free_types_value =
-  Config.declare "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
-val show_free_types = Config.bool show_free_types_value;
+val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
 
 val show_question_marks_default = Unsynchronized.ref true;
 val show_question_marks_value =