# HG changeset patch
# User paulson
# Date 1032515378 -7200
# Node ID 37b22343c35a3fbae2944d3b74076ad08f3ff5f5
# Parent  1681c5b58766a95175b896c02c8609db3e9afd86
shortened a proof

diff -r 1681c5b58766 -r 37b22343c35a src/ZF/Induct/Comb.thy
--- 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->"}. *}