# HG changeset patch
# User paulson
# Date 860146364 -7200
# Node ID c1a00adb0a80df76fc3830edf9638745a72d8442
# Parent  d2ffee4f811bc9fa29525c2fc2668b941f4f66e1
Simplified a proof

diff -r d2ffee4f811b -r c1a00adb0a80 src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Apr 04 11:28:28 1997 +0200
+++ b/src/ZF/func.ML	Fri Apr 04 11:32:44 1997 +0200
@@ -328,9 +328,8 @@
 \         (f Un g) : (A Un C) -> (B Un D)";
 (*Prove the product and domain subgoals using distributive laws*)
 by (asm_full_simp_tac (!simpset addsimps [Pi_iff,extension]@Un_rls) 1);
-by (safe_tac (!claset));
 by (rewtac function_def);
-by (Blast.depth_tac (!claset) 8 1);
+by (Blast_tac 1);
 qed "fun_disjoint_Un";
 
 goal ZF.thy