--- a/FIXME-TODO	Fri Dec 04 15:04:05 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 15:18:33 2009 +0100
@@ -48,3 +48,5 @@
 
 - Check all the places where we do "handle _"
 
+- We shouldn't use the command 'quotient' as this shadows Larry's quotient.
+  Call it 'quotient_type'

--- a/FSet.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/FSet.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -16,14 +16,14 @@
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)
 
-lemma equiv_list_eq:
-  shows "EQUIV list_eq"
-  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+lemma equivp_list_eq:
+  shows "equivp list_eq"
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
 quotient fset = "'a list" / "list_eq"
-  apply(rule equiv_list_eq)
+  apply(rule equivp_list_eq)
   done
 
 print_theorems
@@ -59,7 +59,7 @@
 term FUNION
 thm FUNION_def
 
-thm QUOTIENT_fset
+thm Quotient_fset
 
 thm QUOT_TYPE_I_fset.thm11
 
@@ -418,7 +418,7 @@
 done
 
 quotient fset2 = "'a list" / "list_eq"
-  apply(rule equiv_list_eq)
+  apply(rule equivp_list_eq)
   done
 
 quotient_def
@@ -431,7 +431,7 @@
 where
   "INSERT2 \<equiv> op #"
 
-ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
+ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 

--- a/IntEx.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -9,13 +9,13 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
-  apply(unfold EQUIV_def)
+  apply(unfold equivp_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
 thm quotient_thm
 
-thm my_int_equiv
+thm my_int_equivp
 
 print_theorems
 print_quotients
@@ -198,30 +198,30 @@
 
 
 lemma foldr_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
 apply (induct l)
-apply (simp add: QUOTIENT_ABS_REP[OF b])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 lemma foldl_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
 apply (induct l arbitrary:e)
-apply (simp add: QUOTIENT_ABS_REP[OF a])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 lemma map_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 apply (induct l)
 apply (simp)
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 
@@ -231,10 +231,10 @@
 by simp
 
 lemma cons_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
+  assumes a: "Quotient R1 abs1 rep1"
   shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
   apply (induct t)
-by (simp_all add: QUOTIENT_ABS_REP[OF a])
+by (simp_all add: Quotient_ABS_REP[OF a])
 
 lemma cons_rsp[quotient_rsp]:
   "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
@@ -264,7 +264,7 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: nil_prs)
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -276,8 +276,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
-apply(simp only: cons_prs[OF QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
 done
 

--- a/QuotList.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -2,7 +2,7 @@
 imports QuotScript
 begin
 
-lemma LIST_map_I:
+lemma LIST_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
 
@@ -28,10 +28,10 @@
   shows "LIST_REL R x x"
 by (induct x) (auto simp add: a)
 
-lemma LIST_EQUIV:
-  assumes a: "EQUIV R"
-  shows "EQUIV (LIST_REL R)"
-unfolding EQUIV_def
+lemma LIST_equivp:
+  assumes a: "equivp R"
+  shows "equivp (LIST_REL R)"
+unfolding equivp_def
 apply(rule allI)+
 apply(induct_tac x y rule: list_induct2')
 apply(simp)
@@ -46,70 +46,70 @@
 apply(simp)
 apply(simp)
 using a
-apply(unfold EQUIV_def)
+apply(unfold equivp_def)
 apply(auto)[1]
 apply(metis LIST_REL.simps(4))
 done
 
 lemma LIST_REL_REL: 
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
 apply(induct r s rule: list_induct2')
 apply(simp_all)
-using QUOTIENT_REL[OF q]
+using Quotient_REL[OF q]
 apply(metis)
 done
 
-lemma LIST_QUOTIENT:
-  assumes q: "QUOTIENT R Abs Rep"
-  shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)"
-unfolding QUOTIENT_def
+lemma LIST_Quotient:
+  assumes q: "Quotient R Abs Rep"
+  shows "Quotient (LIST_REL R) (map Abs) (map Rep)"
+unfolding Quotient_def
 apply(rule conjI)
 apply(rule allI)
 apply(induct_tac a)
 apply(simp)
-apply(simp add: QUOTIENT_ABS_REP[OF q])
+apply(simp add: Quotient_ABS_REP[OF q])
 apply(rule conjI)
 apply(rule allI)
 apply(induct_tac a)
 apply(simp)
 apply(simp)
-apply(simp add: QUOTIENT_REP_REFL[OF q])
+apply(simp add: Quotient_REP_reflp[OF q])
 apply(rule allI)+
 apply(rule LIST_REL_REL[OF q])
 done
 
 lemma CONS_PRS:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
-by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q])
+by (induct t) (simp_all add: Quotient_ABS_REP[OF q])
 
 lemma CONS_RSP:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   and     a: "R h1 h2" "LIST_REL R t1 t2"
   shows "LIST_REL R (h1#t1) (h2#t2)"
 using a by (auto)
 
 lemma NIL_PRS:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "[] = (map Abs [])"
 by (simp)
 
 lemma NIL_RSP:
-  assumes q: "QUOTIENT R Abs Rep"
+  assumes q: "Quotient R Abs Rep"
   shows "LIST_REL R [] []"
 by simp
 
 lemma MAP_PRS:
-  assumes q1: "QUOTIENT R1 Abs1 Rep1"
-  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
   shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
 by (induct l)
-   (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2])
+   (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2])
 
 lemma MAP_RSP:
-  assumes q1: "QUOTIENT R1 Abs1 Rep1"
-  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
   and     a: "(R1 ===> R2) f1 f2" 
   and     b: "LIST_REL R1 l1 l2"
   shows "LIST_REL R2 (map f1 l1) (map f2 l2)"

--- a/QuotMain.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -9,7 +9,7 @@
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
-  assumes equiv: "EQUIV R"
+  assumes equiv: "equivp R"
   and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
   and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
@@ -29,10 +29,10 @@
 lemma lem9:
   shows "R (Eps (R x)) = R x"
 proof -
-  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+  have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def)
   then have "R x (Eps (R x))" by (rule someI)
   then show "R (Eps (R x)) = R x"
-    using equiv unfolding EQUIV_def by simp
+    using equiv unfolding equivp_def by simp
 qed
 
 theorem thm10:
@@ -53,7 +53,7 @@
 lemma REP_refl:
   shows "R (REP a) (REP a)"
 unfolding REP_def
-by (simp add: equiv[simplified EQUIV_def])
+by (simp add: equiv[simplified equivp_def])
 
 lemma lem7:
   shows "(R x = R y) = (Abs (R x) = Abs (R y))"
@@ -66,7 +66,7 @@
 theorem thm11:
   shows "R r r' = (ABS r = ABS r')"
 unfolding ABS_def
-by (simp only: equiv[simplified EQUIV_def] lem7)
+by (simp only: equiv[simplified equivp_def] lem7)
 
 
 lemma REP_ABS_rsp:
@@ -74,13 +74,13 @@
   and   "R (REP (ABS g)) f = R g f"
 by (simp_all add: thm10 thm11)
 
-lemma QUOTIENT:
-  "QUOTIENT R ABS REP"
-apply(unfold QUOTIENT_def)
+lemma Quotient:
+  "Quotient R ABS REP"
+apply(unfold Quotient_def)
 apply(simp add: thm10)
 apply(simp add: REP_refl)
 apply(subst thm11[symmetric])
-apply(simp add: equiv[simplified EQUIV_def])
+apply(simp add: equiv[simplified equivp_def])
 done
 
 lemma R_trans:
@@ -88,18 +88,18 @@
   and     bc: "R b c"
   shows "R a c"
 proof -
-  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+  have tr: "transp R" using equiv equivp_reflp_symp_transp[of R] by simp
   moreover have ab: "R a b" by fact
   moreover have bc: "R b c" by fact
-  ultimately show "R a c" unfolding TRANS_def by blast
+  ultimately show "R a c" unfolding transp_def by blast
 qed
 
 lemma R_sym:
   assumes ab: "R a b"
   shows "R b a"
 proof -
-  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  then show "R b a" using ab unfolding SYM_def by blast
+  have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp
+  then show "R b a" using ab unfolding symp_def by blast
 qed
 
 lemma R_trans2:
@@ -128,8 +128,8 @@
     then show "a = b" using rep_inverse by simp
   next
     assume ab: "a = b"
-    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+    have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp
+    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
   qed
   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
 qed
@@ -146,7 +146,7 @@
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
 lemmas [quotient_thm] = 
-  FUN_QUOTIENT LIST_QUOTIENT
+  FUN_Quotient LIST_Quotient
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -265,7 +265,7 @@
     val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata
-    val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
+    val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
   in
     (rty, rel, rel_refl, rel_eqv)
   end
@@ -278,7 +278,7 @@
     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
     val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
-    val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+    val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
   in
     (trans2, reps_same, absrep, quot)
   end
@@ -455,13 +455,13 @@
 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 by auto
 
-(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
-     rtac @{thm IDENTITY_EQUIV},
-     rtac @{thm LIST_EQUIV}])
+     rtac @{thm IDENTITY_equivp},
+     rtac @{thm LIST_equivp}])
 *}
 
 ML {*
@@ -474,7 +474,7 @@
       (ogl as ((Const (@{const_name "Ball"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
@@ -498,7 +498,7 @@
       (ogl as ((Const (@{const_name "Bex"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
@@ -542,7 +542,7 @@
       (ogl as ((Const (@{const_name "Ball"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 (*        val _ = tracing (Syntax.string_of_term ctxt glc);*)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
@@ -573,7 +573,7 @@
       (ogl as ((Const (@{const_name "Bex"}, _)) $
         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
       (let
-        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+        val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 (*        val _ = tracing (Syntax.string_of_term ctxt glc); *)
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
@@ -594,8 +594,8 @@
   end
 *}
 
-lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: EQUIV_REFL)
+lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: equivp_reflp)
 
 ML {*
 fun regularize_tac ctxt rel_eqvs =
@@ -724,7 +724,7 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm IDENTITY_QUOTIENT},
+    [rtac @{thm IDENTITY_Quotient},
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
@@ -776,7 +776,7 @@
   end
 *}
 
-(* It proves the QUOTIENT assumptions by calling quotient_tac *)
+(* It proves the Quotient assumptions by calling quotient_tac *)
 ML {*
 fun solve_quotient_assum i ctxt thm =
   let
@@ -1088,7 +1088,7 @@
  - Rewriting with definitions from the argument defs
      NewConst  ---->  (rep ---> abs) oldConst
 
- - QUOTIENT_REL_REP:
+ - Quotient_REL_REP:
      Rel (Rep x) (Rep y)  ---->  x = y
 
  - ABS_REP
@@ -1107,9 +1107,9 @@
     val thy = ProofContext.theory_of lthy;
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
+    val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
-    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
+    val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1237,7 +1237,7 @@
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
-      val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
+      val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv
       val quotients = quotient_rules_get lthy
       val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
       val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}

--- a/quotient.ML	Fri Dec 04 15:04:05 2009 +0100
+++ b/quotient.ML	Fri Dec 04 15:18:33 2009 +0100
@@ -102,13 +102,13 @@
 (* proves the quotient theorem *)
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
-  val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
+  val quotient_const = Const (@{const_name "Quotient"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
 
   val typedef_quotient_thm_tac =
     EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
-            rtac @{thm QUOT_TYPE.QUOTIENT},
+            rtac @{thm QUOT_TYPE.Quotient},
             rtac quot_type_thm]
 in
   Goal.prove lthy [] [] goal
@@ -146,7 +146,7 @@
 
   (* quotient theorem *)
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
-  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+  val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 
   (* storing the quot-info *)
   val qty_str = fst (Term.dest_Type abs_ty)
@@ -157,7 +157,7 @@
   (* FIXME: to recalculated in for example REGULARIZE *)
 
   (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3
+  val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -205,9 +205,9 @@
 let
   fun mk_goal (rty, rel) =
   let
-    val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+    val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
-    HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel)
+    HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list