diff -r cedfe2a71298 -r 970e86082cd7 Quot/quotient_term.ML
--- 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