# HG changeset patch
# User paulson
# Date 1184605897 -7200
# Node ID 73dbab55d28313ddd1de69e0d5467cd5268ddc10
# Parent  cdaa6b7015097bedd80a7788f1cfef7353cfeee9
tidied

diff -r cdaa6b701509 -r 73dbab55d283 src/HOL/Lambda/Commutation.thy
--- 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"