# HG changeset patch
# User blanchet
# Date 1369660481 -7200
# Node ID 7fd0b5cfbb798dac47c5d48027f69b92c60f96e0
# Parent  ec337c3438a77a605c95e62ead71794864289f1e
get rid of "show_all_types" in Nitpick

diff -r ec337c3438a7 -r 7fd0b5cfbb79 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 27 15:13:34 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 27 15:14:41 2013 +0200
@@ -943,8 +943,8 @@
                                    T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
-            [Syntax.pretty_term (set_show_all_types ctxt) t1,
-             Pretty.str oper, Syntax.pretty_term ctxt t2])
+            [Syntax.pretty_term ctxt t1, Pretty.str oper,
+             Syntax.pretty_term ctxt t2])
       end
     fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
       Pretty.block (Pretty.breaks
diff -r ec337c3438a7 -r 7fd0b5cfbb79 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon May 27 15:13:34 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon May 27 15:14:41 2013 +0200
@@ -142,10 +142,9 @@
    handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
 
 fun quintuple_for_scope code_type code_term code_string
-        ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
+        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
          datatypes, ...} : scope) =
   let
-    val ctxt = set_show_all_types ctxt0
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
                      @{typ bisim_iterator}]
     val (iter_assigns, card_assigns) =
diff -r ec337c3438a7 -r 7fd0b5cfbb79 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 15:13:34 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 15:14:41 2013 +0200
@@ -72,7 +72,6 @@
   val eta_expand : typ list -> term -> int -> term
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
-  val set_show_all_types : Proof.context -> Proof.context
   val indent_size : int
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
@@ -288,11 +287,6 @@
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
 
-fun set_show_all_types ctxt =
-  Config.put show_all_types
-    (Config.get ctxt show_types orelse Config.get ctxt show_sorts
-      orelse Config.get ctxt show_all_types) ctxt
-
 val indent_size = 2
 
 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "