# [isabelle] quotient package: descending method raises type unification error

Hello all,
I tried to test the higher-order lifting capabilities of the
Isabelle2011-1 quotient package recently. Here is my example theory:
theory Scratch
imports "~~/src/HOL/Quotient_Examples/FSet"
begin
lemma "concat_fset (map_fset (map_fset f) xss) = map_fset f (concat_fset xss)"
apply descending
*** Type unification failed: Clash of types "_ list" and "_ fset"
***
*** Type error in application: incompatible operand type
***
*** Operator: map :: ('b fset \<Rightarrow> 'a fset) \<Rightarrow> 'b
fset list \<Rightarrow> 'a fset list
*** Operand: map f :: 'b list \<Rightarrow> 'a list
A recent development version (4ecf63349466) yields exactly the same
error message.
To test whether the multiple occurrences of map_fset at different
types were causing the problem, I tried a simpler example:
lemma "concat_fset (map_fset (\<lambda>x. {|x|}) xs) = xs"
apply descending
*** Type unification failed: Clash of types "_ list" and "_ fset"
***
*** Type error in application: incompatible operand type
***
*** Operator: map :: ('a \<Rightarrow> 'a fset) \<Rightarrow> 'a list
\<Rightarrow> 'a fset list
*** Operand: \<lambda>x. [x] :: 'a \<Rightarrow> 'a list
Is there some additional configuration/setup I need to do to enable
lifting of higher-order theorems, or does this error indicate a bug in
the quotient package?
Also, can anyone suggest *any* examples of higher-order theorems upon
which the descending method actually works? I can't seem to find one.
- Brian

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*