Tidied. Also better proof using new blast_tac

--- a/src/HOL/Lambda/Commutation.ML	Tue Dec 23 11:49:46 1997 +0100
+++ b/src/HOL/Lambda/Commutation.ML	Tue Dec 23 11:50:36 1997 +0100
@@ -35,8 +35,8 @@
 goalw Commutation.thy [commute_def]
  "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
-                     addEs [r_into_rtrancl]
-                     addss simpset()) 1);
+                       addEs [r_into_rtrancl]
+                       addss simpset()) 1);
 qed "square_rtrancl_reflcl_commute";
 
 (*** commute ***)
@@ -68,7 +68,7 @@
 goalw Commutation.thy [diamond_def]
   "!!R. square R R (R^=) (R^=) ==> confluent R";
 by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
-                      addEs [square_subset]) 1);
+                       addEs [square_subset]) 1);
 qed "square_reflcl_confluent";
 
 goal Commutation.thy
@@ -80,8 +80,8 @@
 
 goal Commutation.thy
   "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
-by (fast_tac (claset() addIs [diamond_confluent]
-                    addDs [rtrancl_subset RS sym] addss simpset()) 1);
+by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
+		       addss simpset()) 1);
 qed "diamond_to_confluence";
 
 (*** Church_Rosser ***)
@@ -94,6 +94,6 @@
        rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (etac rtrancl_induct 1);
  by (Blast_tac 1);
-by (Blast.depth_tac (claset() delrules [rtrancl_refl] 
-                       addIs [r_into_rtrancl, rtrancl_trans]) 12 1);
+by (blast_tac (claset() delrules [rtrancl_refl] 
+                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";