--- a/Quot/QuotList.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotList.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -183,9 +183,7 @@
 apply (simp_all)
 done
 
-(* Rest are unused *)
-
-lemma list_rel_eq:
+lemma list_rel_eq[id_simps]:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
@@ -194,6 +192,8 @@
 apply(simp_all)
 done
 
+(* Rest are unused *)
+
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"

--- a/Quot/QuotMain.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotMain.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -109,8 +109,8 @@
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection, symmetric]
   id_o[THEN eq_reflection]
-  o_id[THEN eq_reflection] 
-
+  o_id[THEN eq_reflection]
+  eq_comp_r
 
 (* The translation functions for the lifting process. *)
 use "quotient_term.ML" 

--- a/Quot/QuotScript.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -509,6 +509,12 @@
   apply(simp add: Quotient_abs_rep[OF a])
   done
 
+lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply auto
+  done
+
 lemma fun_rel_eq_rel:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"

--- a/Quot/quotient_term.ML	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 08 10:39:08 2010 +0100
@@ -215,8 +215,9 @@
   map_types (Envir.subst_type ty_inst) trm
 end
 
-fun mk_rel_compose (trm1, trm2) = 
-  Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ trm2
+fun mk_rel_compose (trm1, trm2) =
+  Const (@{const_name "pred_comp"}, dummyT) $ trm1 $
+   (Const (@{const_name "pred_comp"}, dummyT) $ trm2 $ trm1)
 
 fun get_relmap ctxt s =
 let
@@ -288,7 +289,7 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           mk_rel_compose (eqv_rel', result)
+           mk_rel_compose (result, eqv_rel')
          end  
       | _ => HOLogic.eq_const rty
 
@@ -385,7 +386,7 @@
          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
        in
          if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -393,7 +394,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
@@ -401,20 +402,20 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
-         else equiv_relation ctxt (domain_type ty, domain_type ty') 
+         else new_equiv_relation ctxt (domain_type ty, domain_type ty') 
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
          val rel_ty = fastype_of rel
-         val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') 
+         val rel' = new_equiv_relation ctxt (domain_type rel_ty, domain_type ty') 
        in 
          if rel' aconv rel then rtrm else raise exc
        end