--- a/Quot/Examples/AbsRepTest.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -93,8 +93,8 @@
 
 ML {*
 test_funs absF @{context} 
-     (@{typ "('a list) list \<Rightarrow> 'a"}, 
-      @{typ "('a fset) fset \<Rightarrow> 'a"})
+     (@{typ "('a list) list \<Rightarrow> 'a list"}, 
+      @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}
 
 

--- a/Quot/Examples/FSet3.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -600,5 +600,7 @@
 apply (lifting list.cases(2))
 done
 
+thm quot_respect
+
 
 end

--- a/Quot/QuotList.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/QuotList.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -125,7 +125,7 @@
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma foldr_prs[quot_respect]:
+lemma foldr_prs[quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"

--- a/Quot/quotient_term.ML	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 26 23:20:46 2009 +0100
@@ -228,7 +228,7 @@
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 
-(* FIXME: check that the types correspond to each other? *)
+(* FIXME: check that the types correspond to each other *)
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty