--- a/Quot/QuotScript.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/QuotScript.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -256,7 +256,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: Respects_def in_respects)
+  apply(simp add: in_respects)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -338,6 +338,12 @@
   using Quotient_rel[OF q]
   by metis
 
+(* needed for regularising? *)
+lemma babs_reg_eqv:
+  shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
+by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
+
+
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"