--- a/src/ZF/Induct/Comb.thy Fri Sep 20 11:49:06 2002 +0200
+++ b/src/ZF/Induct/Comb.thy Fri Sep 20 11:49:38 2002 +0200
@@ -177,8 +177,8 @@
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
apply (erule rtrancl_induct)
apply (blast intro: reduction_rls)
- apply (erule trans_rtrancl [THEN transD])
- apply (blast intro: contract_combD2 reduction_rls)
+ apply (blast intro: trans_rtrancl [THEN transD]
+ contract_combD2 reduction_rls)
done
text {* Counterexample to the diamond property for @{text "-1->"}. *}