--- 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
--- 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) =
--- 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 " "