--- a/QuotScript.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/QuotScript.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -461,8 +461,8 @@
   done
 
 lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
-  shows "All P ==> Ball R Q"
+  assumes a: "\<And>x :: 'a. (R x \<Longrightarrow> P x \<longrightarrow> Q x)"
+  shows "All P \<longrightarrow> Ball R Q"
   using a
   apply (metis COMBC_def Collect_def Collect_mem_eq a)
   done