# HG changeset patch
# User blanchet
# Date 1391171360 -3600
# Node ID f7358e55018faeb0566eec47e22d7de231e58bc6
# Parent  8450622db0c5e8dd544aea17be08dfd2e826ae6b
tuning

diff -r 8450622db0c5 -r f7358e55018f src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 12:30:54 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Jan 31 13:29:20 2014 +0100
@@ -746,7 +746,7 @@
      qed
     }
     ultimately show ?thesis unfolding bij_betw_def inj_on_def
-    by (metis image_subsetI order_eq_iff subsetI)
+    by (metis (no_types) image_subsetI order_eq_iff subsetI)
   qed
   thus ?thesis using card_of_ordIso by blast
 qed