--- a/src/HOL/Lambda/Commutation.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Lambda/Commutation.thy Wed Dec 06 01:12:36 2006 +0100
@@ -130,8 +130,9 @@
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
- [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
- rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
+ [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
+ thm "rtrancl_converseI", thm "converseI",
+ thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
apply (erule rtrancl_induct)
apply blast
apply (blast del: rtrancl_refl intro: rtrancl_trans)