diff -r d1742d1b7f0f -r 249fa34faba2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Fun.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -21,6 +21,7 @@
 lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
   by (force intro: theI')
 
+
 subsection \<open>The Identity Function \<open>id\<close>\<close>
 
 definition id :: "'a \<Rightarrow> 'a"
@@ -283,9 +284,8 @@
   shows "inj f"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
 proof (rule inj_onI)
-  fix x y
-  assume f_eq: "f x = f y"
-  show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
+  show "x = y" if "f x = f y" for x y
+   by (rule linorder_cases) (auto dest: hyp simp: that)
 qed
 
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
@@ -427,9 +427,8 @@
   by (auto simp add: bij_betw_def)
 
 lemma bij_betw_combine:
-  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
-  shows "bij_betw f (A \<union> C) (B \<union> D)"
-  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
+  "bij_betw f A B \<Longrightarrow> bij_betw f C D \<Longrightarrow> B \<inter> D = {} \<Longrightarrow> bij_betw f (A \<union> C) (B \<union> D)"
+  unfolding bij_betw_def inj_on_Un image_Un by auto
 
 lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<le> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
   by (auto simp add: bij_betw_def inj_on_def)
@@ -531,14 +530,15 @@
     and img2: "f' ` A' \<le> A"
   shows "bij_betw f A A'"
   using assms
-proof (unfold bij_betw_def inj_on_def, safe)
+  unfolding bij_betw_def inj_on_def
+proof safe
   fix a b
   assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
   with ** show "a = b" by simp
 next
   fix a' assume *: "a' \<in> A'"
-  hence "f' a' \<in> A" using img2 by blast
+  then have "f' a' \<in> A" using img2 by blast
   moreover
   have "a' = f (f' a')" using * right by simp
   ultimately show "a' \<in> f ` A" by blast
@@ -823,7 +823,7 @@
 
 subsubsection \<open>Proof tools\<close>
 
-text \<open>Simplify terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
+text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
 
 simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
   let
@@ -843,14 +843,14 @@
       let
         val t = Thm.term_of ct
       in
-        case find_double t of
+        (case find_double t of
           (T, NONE) => NONE
         | (T, SOME rhs) =>
             SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
               (fn _ =>
                 resolve_tac ctxt [eq_reflection] 1 THEN
                 resolve_tac ctxt @{thms ext} 1 THEN
-                simp_tac (put_simpset ss ctxt) 1))
+                simp_tac (put_simpset ss ctxt) 1)))
       end
   in proc end
 \<close>