make Nitpick output everything to tracing in debug mode;
so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 13:24:03 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 13:26:06 2010 +0200
@@ -225,13 +225,15 @@
         o Pretty.chunks o cons (Pretty.str "") o single
         o Pretty.mark Markup.hilite
       else
-        priority o Pretty.string_of
+        (fn s => (priority s; if debug then tracing s else ()))
+        o Pretty.string_of
     (* (unit -> Pretty.T) -> unit *)
     fun pprint_m f = () |> not auto ? pprint o f
     fun pprint_v f = () |> verbose ? pprint o f
     fun pprint_d f = () |> debug ? pprint o f
     (* string -> unit *)
     val print = pprint o curry Pretty.blk 0 o pstrs
+    val print_g = pprint o Pretty.str
     (* (unit -> string) -> unit *)
     val print_m = pprint_m o K o plazy
     val print_v = pprint_v o K o plazy
@@ -265,8 +267,8 @@
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
 (*
-    val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)
-    val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t))
+    val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t)
+    val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t))
                      orig_assm_ts
 *)
     val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -338,7 +340,7 @@
                           | _ => false) finitizes)
     val standard = forall snd stds
 (*
-    val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
+    val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us)
 *)
 
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
@@ -431,10 +433,10 @@
             else
               ()
 (*
-    val _ = priority "Monotonic types:"
-    val _ = List.app (priority o string_for_type ctxt) mono_Ts
-    val _ = priority "Nonmonotonic types:"
-    val _ = List.app (priority o string_for_type ctxt) nonmono_Ts
+    val _ = print_g "Monotonic types:"
+    val _ = List.app (print_g o string_for_type ctxt) mono_Ts
+    val _ = print_g "Nonmonotonic types:"
+    val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts
 *)
 
     val need_incremental = Int.max (max_potential, max_genuine) >= 2
@@ -472,10 +474,10 @@
                 raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
                                  \problem_for_scope", "too large scope")
 (*
-        val _ = priority "Offsets:"
+        val _ = print_g "Offsets:"
         val _ = List.app (fn (T, j0) =>
-                             priority (string_for_type ctxt T ^ " = " ^
-                                       string_of_int j0))
+                             print_g (string_for_type ctxt T ^ " = " ^
+                                    string_of_int j0))
                          (Typtab.dest ofs)
 *)
         val all_exact = forall (is_exact_type datatypes true) all_Ts
@@ -504,7 +506,7 @@
         val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
                             nondef_us
 (*
-        val _ = List.app (priority o string_for_nut ctxt)
+        val _ = List.app (print_g o string_for_nut ctxt)
                          (free_names @ sel_names @ nonsel_names @
                           nondef_us @ def_us)
 *)

--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 13 13:24:03 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 13 13:26:06 2010 +0200
@@ -1130,8 +1130,8 @@
               if is_boolean_type T then
                 bool_rep polar opt
               else
-                smart_range_rep ofs T1 (fn () => card_of_type card_assigns T)
-                                (unopt_rep R1)
+                lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T)
+                               (unopt_rep R1)
                 |> opt ? opt_rep ofs T
           in s_op2 Apply T ran_R u1 u2 end
         | Op2 (Lambda, T, _, u1, u2) =>

--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Apr 13 13:24:03 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Apr 13 13:26:06 2010 +0200
@@ -34,7 +34,7 @@
   val is_one_rep : rep -> bool
   val is_lone_rep : rep -> bool
   val dest_Func : rep -> rep * rep
-  val smart_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
+  val lazy_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
   val binder_reps : rep -> rep list
   val body_rep : rep -> rep
   val one_rep : int Typtab.table -> typ -> rep -> rep
@@ -153,16 +153,16 @@
 fun dest_Func (Func z) = z
   | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
 (* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
-fun smart_range_rep _ _ _ Unit = Unit
-  | smart_range_rep _ _ _ (Vect (_, R)) = R
-  | smart_range_rep _ _ _ (Func (_, R2)) = R2
-  | smart_range_rep ofs T ran_card (Opt R) =
-    Opt (smart_range_rep ofs T ran_card R)
-  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
+fun lazy_range_rep _ _ _ Unit = Unit
+  | lazy_range_rep _ _ _ (Vect (_, R)) = R
+  | lazy_range_rep _ _ _ (Func (_, R2)) = R2
+  | lazy_range_rep ofs T ran_card (Opt R) =
+    Opt (lazy_range_rep ofs T ran_card R)
+  | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
     Atom (1, offset_of_type ofs T2)
-  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
+  | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
     Atom (ran_card (), offset_of_type ofs T2)
-  | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
+  | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R])
 
 (* rep -> rep list *)
 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2