# HG changeset patch
# User wenzelm
# Date 1283522043 -7200
# Node ID a00da1674c1cceebe427a2bcbb97c7fd0b3454e3
# Parent  240e2b41a041e238b7a0fd2516700e485157c99a
turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;

diff -r 240e2b41a041 -r a00da1674c1c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 03 14:20:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 03 15:54:03 2010 +0200
@@ -945,13 +945,13 @@
         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt full_types i n =
+fun string_for_proof ctxt0 full_types i n =
   let
+    val ctxt = Config.put show_free_types false ctxt0
     fun fix_print_mode f x =
-      setmp_CRITICAL show_no_free_types true
-          (setmp_CRITICAL show_types true
-               (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                                         (print_mode_value ())) f)) x
+      setmp_CRITICAL show_types true
+           (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                                     (print_mode_value ())) f) x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
diff -r 240e2b41a041 -r a00da1674c1c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 14:20:47 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 15:54:03 2010 +0200
@@ -392,7 +392,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_question_marks_value #>
+ (register_config Syntax.show_free_types_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 #>
diff -r 240e2b41a041 -r a00da1674c1c src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Sep 03 14:20:47 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 15:54:03 2010 +0200
@@ -9,7 +9,9 @@
   val show_brackets: bool Unsynchronized.ref
   val show_sorts: bool Unsynchronized.ref
   val show_types: bool Unsynchronized.ref
-  val show_no_free_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
   val show_question_marks_default: bool Unsynchronized.ref
@@ -51,10 +53,14 @@
 val show_types = Unsynchronized.ref false;
 val show_sorts = Unsynchronized.ref false;
 val show_brackets = Unsynchronized.ref false;
-val show_no_free_types = Unsynchronized.ref false;
 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 false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
+val show_free_types = Config.bool show_free_types_value;
+
 val show_question_marks_default = Unsynchronized.ref true;
 val show_question_marks_value =
   Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
@@ -120,8 +126,9 @@
 (** term_to_ast **)
 
 fun ast_of_term idents consts ctxt trf
-    show_all_types no_freeTs show_types show_sorts show_structs tm =
+    show_all_types show_types show_sorts show_structs tm =
   let
+    val show_free_types = Config.get ctxt show_free_types;
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, T)) $ u) =
@@ -148,11 +155,11 @@
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
           else (t, t :: seen)
       | prune_typs (t as Var (xi, ty), seen) =
           if ty = dummyT then (t, seen)
-          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
           else (t, t :: seen)
       | prune_typs (t_seen as (Bound _, _)) = t_seen
       | prune_typs (Abs (x, ty, t), seen) =
@@ -199,7 +206,7 @@
   end;
 
 fun term_to_ast idents consts ctxt trf tm =
-  ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+  ast_of_term idents consts ctxt trf (! show_all_types)
     (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
 
 
diff -r 240e2b41a041 -r a00da1674c1c src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri Sep 03 14:20:47 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 15:54:03 2010 +0200
@@ -63,8 +63,10 @@
 
 in
 
-fun pretty_goals ctxt {total, main, maxgoals} state =
+fun pretty_goals ctxt0 {total, main, maxgoals} state =
   let
+    val ctxt = Config.put show_free_types false ctxt0;
+
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
     val prt_term = Syntax.pretty_term ctxt;
@@ -115,9 +117,8 @@
       (if types then pretty_vars prop else []) @
       (if sorts then pretty_varsT prop else []);
   in
-    setmp_CRITICAL show_no_free_types true
-      (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
-        (setmp_CRITICAL show_sorts false pretty_gs))
+    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+      (setmp_CRITICAL show_sorts false pretty_gs)
    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   end;