diff -r cfd2a42d60e3 -r 64874975f087 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Feb 01 09:04:22 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Feb 01 09:47:46 2010 +0100
@@ -388,7 +388,7 @@
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_bex1 = Const (@{const_name Bex1}, dummyT)
-val mk_bexeq = Const (@{const_name Bex1_rel}, dummyT)
+val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
 (* - applies f to the subterm of an abstraction, 
@@ -477,7 +477,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
-         else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
@@ -510,7 +510,7 @@
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
-         else mk_bexeq $ resrel $ subtrm
+         else mk_bex1_rel $ resrel $ subtrm
        end
 
   | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
@@ -521,7 +521,7 @@
        in
          if resrel <> needrel
          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
-         else mk_bexeq $ resrel $ subtrm
+         else mk_bex1_rel $ resrel $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *)