Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.

--- a/src/HOL/Quotient_Examples/FSet.thy	Sat Feb 04 17:01:25 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sun Feb 05 07:05:34 2012 +0100
@@ -934,15 +934,15 @@
 
 lemma concat_empty_fset [simp]:
   shows "concat_fset {||} = {||}"
-  by (lifting concat.simps(1))
+  by descending simp
 
 lemma concat_insert_fset [simp]:
   shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
-  by (lifting concat.simps(2))
+  by descending simp
 
 lemma concat_inter_fset [simp]:
   shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
-  by (lifting concat_append)
+  by descending simp
 
 lemma map_concat_fset:
   shows "map_fset f (concat_fset xs) = concat_fset (map_fset (map_fset f) xs)"

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 04 17:01:25 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Feb 05 07:05:34 2012 +0100
@@ -728,7 +728,7 @@
           | matches ((rty, qty)::tail) =
               (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
                 NONE => matches tail
-              | SOME inst => Envir.subst_type inst qty)
+              | SOME inst => subst_typ ctxt ty_subst (Envir.subst_type inst qty))
       in
         matches ty_subst
       end
@@ -749,7 +749,7 @@
           | matches ((rconst, qconst)::tail) =
               (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
                 NONE => matches tail
-              | SOME inst => Envir.subst_term inst qconst)
+              | SOME inst => subst_trm ctxt ty_subst trm_subst (Envir.subst_term inst qconst))
       in
         matches trm_subst
       end