# HG changeset patch
# User blanchet
# Date 1330899643 -3600
# Node ID 9b38f85275108997024ea3abfc356c933150ff0f
# Parent  2a28e66e2e4c604a9f7fd030b81304e4e76e6cfd
addressed a quotient-type-related issue that arose with the port to "set"

diff -r 2a28e66e2e4c -r 9b38f8527510 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 04 23:20:43 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 04 23:20:43 2012 +0100
@@ -744,8 +744,8 @@
     try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
     = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
   | is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (s, Type (@{type_name fun},
-                                         [abs_T as Type (abs_s, _), _]))) =
+fun is_quot_rep_fun ctxt (s, Type (@{type_name fun},
+                                   [abs_T as Type (abs_s, _), _])) =
     (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
        SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
      | NONE => false)
@@ -1767,16 +1767,21 @@
                       is_quot_type ctxt (range_type T) then
                 let
                   val abs_T = range_type T
-                  val rep_T = domain_type (domain_type T)
+                  val rep_T = elem_type (domain_type T)
                   val eps_fun = Const (@{const_name Eps},
                                        (rep_T --> bool_T) --> rep_T)
                   val normal_fun =
                     Const (quot_normal_name_for_type ctxt abs_T,
                            rep_T --> rep_T)
                   val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
+                  val pred =
+                    Abs (Name.uu, rep_T,
+                         Const (@{const_name Set.member},
+                                rep_T --> domain_type T --> bool_T)
+                         $ Bound 0 $ Bound 1)
                 in
-                  (Abs (Name.uu, rep_T --> bool_T,
-                        abs_fun $ (normal_fun $ (eps_fun $ Bound 0)))
+                  (Abs (Name.uu, HOLogic.mk_setT rep_T,
+                        abs_fun $ (normal_fun $ (eps_fun $ pred)))
                    |> do_term (depth + 1) Ts, ts)
                 end
               else if is_rep_fun ctxt x then