# HG changeset patch
# User wenzelm
# Date 1470170213 -7200
# Node ID 8d20875f1290a086d65218e4480dbe84372b2576
# Parent  4854f7ee0987438a0887913441e903977e73a507
tuned proof;

diff -r 4854f7ee0987 -r 8d20875f1290 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Aug 02 21:55:15 2016 +0200
+++ b/src/HOL/Fun.thy	Tue Aug 02 22:36:53 2016 +0200
@@ -411,7 +411,7 @@
 qed
 
 lemma bij_betw_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
-  unfolding bij_betw_def inj_on_def by force  (* slow *)
+  unfolding bij_betw_def inj_on_def by safe force+  (* somewhat slow *)
 
 lemma bij_betw_id[intro, simp]: "bij_betw id A A"
   unfolding bij_betw_def id_def by auto