# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 096697aec8a74a76cb56e7bd241e3797dcde8d98
# Parent  447cda88adfec014a53b2b437b65ef6ad294513e
rationalized output (a bit)

diff -r 447cda88adfe -r 096697aec8a7 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -235,20 +235,19 @@
          show_skolems, show_consts, evals, formats, atomss, max_potential,
          max_genuine, check_potential, check_genuine, batch_size, ...} = params
     val state_ref = Unsynchronized.ref state
-    val pprint =
+    fun pprint print =
       if mode = Auto_Try then
         Unsynchronized.change state_ref o Proof.goal_message o K
         o Pretty.chunks o cons (Pretty.str "") o single
         o Pretty.mark Isabelle_Markup.hilite
       else
-        (fn s => (Output.urgent_message s; if debug then tracing s else ()))
-        o Pretty.string_of
-    fun pprint_n f = () |> mode = Normal ? pprint o f
-    fun pprint_v f = () |> verbose ? pprint o f
-    fun pprint_d f = () |> debug ? pprint o f
-    val print = pprint o curry Pretty.blk 0 o pstrs
+        print o Pretty.string_of
+    fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
+    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
+    fun pprint_d f = () |> debug ? pprint tracing o f
+    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
 (*
-    val print_g = pprint o Pretty.str
+    val print_g = pprint tracing o Pretty.str
 *)
     val print_n = pprint_n o K o plazy
     val print_v = pprint_v o K o plazy
@@ -323,7 +322,7 @@
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
     fun print_wf (x, (gfp, wf)) =
-      pprint (Pretty.blk (0,
+      pprint_n (fn () => Pretty.blk (0,
           pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
           @ Syntax.pretty_term ctxt (Const x) ::
           pstrs (if wf then
@@ -672,7 +671,7 @@
           codatatypes_ok
         fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
       in
-        (pprint (Pretty.chunks
+        (pprint_n (fn () => Pretty.chunks
              [Pretty.blk (0,
                   (pstrs ((if mode = Auto_Try then "Auto " else "") ^
                           "Nitpick found a" ^
@@ -881,7 +880,7 @@
           if null scopes then
             print_n (K "The scope specification is inconsistent.")
           else if verbose then
-            pprint (Pretty.chunks
+            pprint_n (fn () => Pretty.chunks
                 [Pretty.blk (0,
                      pstrs ((if n > 1 then
                                "Batch " ^ string_of_int (j + 1) ^ " of " ^
diff -r 447cda88adfe -r 096697aec8a7 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -1815,12 +1815,17 @@
 
 (** Axiom extraction/generation **)
 
-fun extensional_equal j (Type (@{type_name fun}, [dom_T, ran_T])) t1 t2 =
-    let val var_t = Var (("x", j), dom_T) in
+fun extensional_equal j T t1 t2 =
+  if is_fun_type T orelse is_set_like_type T then
+    let
+      val dom_T = pseudo_domain_type T
+      val ran_T = pseudo_range_type T
+      val var_t = Var (("x", j), dom_T)
+    in
       extensional_equal (j + 1) ran_T (betapply (t1, var_t))
                         (betapply (t2, var_t))
     end
-  | extensional_equal _ T t1 t2 =
+  else
     Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
 
 fun equationalize_term ctxt tag t =
@@ -1837,7 +1842,7 @@
           @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
         | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
           @{const Trueprop} $ extensional_equal j T t1 t2
-        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^
+        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
                          quote (Syntax.string_of_term ctxt t) ^ ".");
                 raise SAME ()))
     |> SOME
diff -r 447cda88adfe -r 096697aec8a7 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -786,7 +786,7 @@
                (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
          | Op2 (Subset, _, _, u1, u2) =>
            let
-             val dom_T = elem_type (type_of u1)
+             val dom_T = pseudo_domain_type (type_of u1)
              val R1 = rep_of u1
              val R2 = rep_of u2
              val (dom_R, ran_R) =
diff -r 447cda88adfe -r 096697aec8a7 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -1110,8 +1110,9 @@
       Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
                     shape_tuple T2 R2 (List.drop (us, arity1))])
     end
-  | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
-    Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
+  | shape_tuple T (R as Vect (k, R')) us =
+    Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
+                     (batch_list (length us div k) us))
   | shape_tuple T _ [u] =
     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
   | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)