--- 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)