tidied

--- a/src/HOL/Lambda/Commutation.thy	Mon Jul 16 17:29:34 2007 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Mon Jul 16 19:11:37 2007 +0200
@@ -94,7 +94,7 @@
 lemma diamond_Un:
     "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
   apply (unfold diamond_def)
-  apply (assumption | rule commute_Un commute_sym)+
+  apply (blast intro: commute_Un commute_sym) 
   done
 
 lemma diamond_confluent: "diamond R ==> confluent R"