use matching of types than just equality - this is needed in nominal to cope with type variables

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Aug 24 15:08:05 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Aug 24 22:38:45 2010 +0800
@@ -686,8 +686,8 @@
     rthm 
     |> asm_full_simplify ss
     |> Drule.eta_contraction_rule 
-  val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
-  val goal = derive_qtrm ctxt qtys (prop_of rthm'')
+  val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
+  val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
 in
   Goal.prove ctxt' [] [] goal 
     (K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 24 15:08:05 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Aug 24 22:38:45 2010 +0800
@@ -225,12 +225,16 @@
              val qtyenv = match ctxt absrep_match_err qty_pat qty
              val args_aux = map (double_lookup rtyenv qtyenv) vs
              val args = map (absrep_fun flag ctxt) args_aux
-             val map_fun = mk_mapfun ctxt vs rty_pat
-             val result = list_comb (map_fun, args)
            in
              if forall is_identity args
              then absrep_const flag ctxt s'
-             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+             else 
+               let
+                 val map_fun = mk_mapfun ctxt vs rty_pat
+                 val result = list_comb (map_fun, args)
+               in
+                 mk_fun_compose flag (absrep_const flag ctxt s', result)
+               end
            end
     | (TFree x, TFree x') =>
         if x = x'
@@ -332,14 +336,18 @@
            val qtyenv = match ctxt equiv_match_err qty_pat qty
            val args_aux = map (double_lookup rtyenv qtyenv) vs
            val args = map (equiv_relation ctxt) args_aux
-           val rel_map = mk_relmap ctxt vs rty_pat
-           val result = list_comb (rel_map, args)
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
            if forall is_eq args
            then eqv_rel'
-           else mk_rel_compose (result, eqv_rel')
+           else 
+             let 
+               val rel_map = mk_relmap ctxt vs rty_pat
+               val result = list_comb (rel_map, args)
+             in
+               mk_rel_compose (result, eqv_rel')
+             end
          end
       | _ => HOLogic.eq_const rty
 
@@ -740,10 +748,14 @@
      false: raw -> quotient
 *)
 fun mk_ty_subst qtys direction ctxt =
+let
+  val thy = ProofContext.theory_of ctxt  
+in
   Quotient_Info.quotdata_dest ctxt
    |> map (fn x => (#rtyp x, #qtyp x))
-   |> filter (fn (_, qty) => member (op =) qtys qty)
+   |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
    |> map (if direction then swap else I)
+end
 
 fun mk_trm_subst qtys direction ctxt =
 let