# HG changeset patch
# User paulson
# Date 828611005 -7200
# Node ID 46d2d4a249caab3eda61e06c169272e5866a7dc5
# Parent  581165679095cd958a8c8375a4f891b264a42f1b
For renaming to rtrancl_Un_rtrancl

diff -r 581165679095 -r 46d2d4a249ca src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Thu Apr 04 11:41:35 1996 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Thu Apr 04 11:43:25 1996 +0200
@@ -80,8 +80,8 @@
 goal Commutation.thy
  "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
 \      ==> confluent(R Un S)";
-br(trancl_Un_trancl RS subst) 1;
-by(fast_tac (HOL_cs addDs [diamond_Un] addIs [diamond_confluent]) 1);
+br (rtrancl_Un_rtrancl RS subst) 1;
+by (fast_tac (HOL_cs addDs [diamond_Un] addIs [diamond_confluent]) 1);
 qed "confluent_Un";
 
 goal Commutation.thy