diff -r 693aecde755d -r 1fc2b6f6ea2a Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Fri Jan 15 15:56:06 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 15 15:56:25 2010 +0100
@@ -301,8 +301,6 @@
   done
 
 lemma bex_reg_eqv_range:
-  fixes P::"'a \<Rightarrow> bool"
-  and x::"'a"
   assumes a: "equivp R2"
   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
   apply(auto)