# HG changeset patch
# User paulson
# Date 956482772 -7200
# Node ID eae30939b5925c5d6429dc349ad1cfa4535e2ef9
# Parent  1ef6e77e12ee71e086ce60bfc3edc55f8a995d87
this change saves 15 seconds

diff -r 1ef6e77e12ee -r eae30939b592 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sun Apr 23 11:35:00 2000 +0200
+++ b/src/HOL/Fun.ML	Sun Apr 23 11:39:32 2000 +0200
@@ -406,7 +406,7 @@
 qed "bij_image_Collect_eq";
 
 Goal "bij f ==> f -`` A = inv f `` A";
-by Auto_tac;
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
 qed "bij_vimage_eq_inv_image";