# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264678130 -3600
# Node ID 54faefa537453d8347d8fbc5221bb1d4cb04aaeb
# Parent  bc739536b7153857989851e3187c58d6962f6475
End of renaming.

diff -r bc739536b715 -r 54faefa53745 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Jan 28 12:25:38 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 28 12:28:50 2010 +0100
@@ -377,7 +377,7 @@
  but also accepts partially regularized terms.
 
  This means that the raw theorems can have:
-   Ball (Respects R),  Bex (Respects R), Bexeq (Respects R), Babs, R
+   Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
  in the places where:
    All, Ex, Ex1, %, (op =)
  is required the lifted theorem.
@@ -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 Bexeq}, dummyT)
+val mk_bexeq = Const (@{const_name Bex1_rel}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
 (* - applies f to the subterm of an abstraction, 
@@ -503,7 +503,7 @@
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
-  | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')