# HG changeset patch
# User paulson
# Date 905442122 -7200
# Node ID 024d887eae506d0954009fe14894c4438227e6e0
# Parent  079d8eb6db1989200b289d5d41d0d9b1fd395c02
fixed PROOF FAILED

diff -r 079d8eb6db19 -r 024d887eae50 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Sep 10 17:40:03 1998 +0200
+++ b/src/ZF/Zorn.ML	Thu Sep 10 17:42:02 1998 +0200
@@ -217,7 +217,7 @@
 by (rtac CollectI 1 THEN Blast_tac 1);
 by Safe_tac;
 by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Fast_tac);   (*Blast_tac's slow*)
 qed "TFin_chain_lemma4";
 
 Goal "EX c. c : maxchain(S)";
@@ -256,7 +256,7 @@
 by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
 by (rename_tac "c" 1);
 by (res_inst_tac [("x", "Union(c)")] bexI 1);
-by (Fast_tac 2);  (*Blast_tac: PROOF FAILED*)
+by (Blast_tac 2);
 by Safe_tac;
 by (rename_tac "z" 1);
 by (rtac classical 1);