# HG changeset patch
# User blanchet
# Date 1330597736 -3600
# Node ID a6f83f21dc2c1b39e1acb9301c57f8c3802fa45e
# Parent  18ba7f63217d5bc03f33889afb07aeea58f2574a
fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction

diff -r 18ba7f63217d -r a6f83f21dc2c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 01 11:28:56 2012 +0100
@@ -767,7 +767,8 @@
     raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
     let
-      val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s)
+      val {qtyp, equiv_rel, equiv_thm, ...} =
+        the (Quotient_Info.lookup_quotients thy s)
       val partial =
         case prop_of equiv_thm of
           @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
@@ -1785,12 +1786,14 @@
                   else if is_quot_type ctxt (domain_type T) then
                     let
                       val abs_T = domain_type T
-                      val rep_T = domain_type (range_type T)
+                      val rep_T = elem_type (range_type T)
                       val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
                       val (equiv_rel, _) =
                         equiv_relation_for_quot_type ctxt abs_T
                     in
-                      (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
+                      (Abs (Name.uu, abs_T,
+                            HOLogic.Collect_const rep_T
+                            $ (equiv_rel $ (rep_fun $ Bound 0))),
                        ts)
                     end
                   else