tuned;

--- a/src/HOL/Finite_Set.thy	Sat Oct 01 19:29:48 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Oct 01 19:30:21 2016 +0200
@@ -139,12 +139,12 @@
   qed
 qed
 
-lemma finite_conv_nat_seg_image: "finite A \<longleftrightarrow> (\<exists>(n::nat) f. A = f ` {i::nat. i < n})"
+lemma finite_conv_nat_seg_image: "finite A \<longleftrightarrow> (\<exists>n f. A = f ` {i::nat. i < n})"
   by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
 
 lemma finite_imp_inj_to_nat_seg:
   assumes "finite A"
-  shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A"
+  shows "\<exists>f n. f ` A = {i::nat. i < n} \<and> inj_on f A"
 proof -
   from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
   obtain f and n :: nat where bij: "bij_betw f {i. i<n} A"

--- a/src/HOL/Wellfounded.thy	Sat Oct 01 19:29:48 2016 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Oct 01 19:30:21 2016 +0200
@@ -837,8 +837,9 @@
       qed
     qed
   next
-    case [simp]: infinite
-    show ?case by (rule accI) (auto elim: max_ext.cases)
+    case infinite
+    show ?case
+      by (rule accI) (auto elim: max_ext.cases simp: infinite)
   qed
 qed