# HG changeset patch
# User traytel
# Date 1392900806 -3600
# Node ID 48596c45bf7f9736c4ccae41f75b17fd4afce4f3
# Parent  257bd115fcca950c7220e50126cf6e6d48a8293f
less flex-flex pairs (thanks to Lars' statistics)

diff -r 257bd115fcca -r 48596c45bf7f src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 11:40:03 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Feb 20 13:53:26 2014 +0100
@@ -414,7 +414,7 @@
   let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
   have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
   using * unfolding inj_on_def by auto
-  thus ?thesis using card_of_ordLeq by fast
+  thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
 qed
 
 corollary Card_order_singl_ordLeq:
diff -r 257bd115fcca -r 48596c45bf7f src/HOL/BNF_Constructions_on_Wellorders.thy
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Feb 20 11:40:03 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Thu Feb 20 13:53:26 2014 +0100
@@ -1652,8 +1652,7 @@
       qed(insert h, unfold Func_def Func_map_def, auto)
     qed
     moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
-    using inv_into_into j2A2 B1 A2 inv_into_into
-    unfolding j1_def image_def by fast+
+    using j2A2 B1 A2 unfolding j1_def image_def by (fast intro: inv_into_into)+
     ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
     unfolding Func_map_def[abs_def] unfolding image_def by auto
   qed(insert B1 Func_map[OF _ _ A2(2)], auto)