# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1328421934 -3600
# Node ID 5f5665a0b9737f816906b4a10fe65d18aa8b3eb6
# Parent  26153cbe97bf5053265a8ed5eb1720b6dafcf208
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.

diff -r 26153cbe97bf -r 5f5665a0b973 src/HOL/Quotient_Examples/FSet.thy
--- 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)"
diff -r 26153cbe97bf -r 5f5665a0b973 src/HOL/Tools/Quotient/quotient_term.ML
--- 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