# HG changeset patch # User Cezary Kaliszyk # 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')