1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 23 03:34:17 2011 +0900
     1.3 @@ -208,6 +208,13 @@
     1.4          in
     1.5            list_comb (get_mapfun ctxt "fun", [arg1, arg2])
     1.6          end
     1.7 +(* FIXME: use type_name antiquotation if set type becomes explicit *)
     1.8 +    | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) =>
     1.9 +        let
    1.10 +          val arg = absrep_fun (negF flag) ctxt (ty, ty')
    1.11 +        in
    1.12 +          get_mapfun ctxt "Set.set" $ arg
    1.13 +        end
    1.14      | (Type (s, tys), Type (s', tys')) =>
    1.15          if s = s'
    1.16          then