diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -919,7 +919,7 @@
         case 0 then show ?case by simp
       next
         case (Suc n g)
-        def h \<equiv> "\<lambda>z. g z - 1"
+        define h where "h z = g z - 1" for z
         with Suc have "n = h y" by simp
         with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
           by auto
@@ -927,7 +927,7 @@
         then show ?case by (simp add: comp_assoc hyp)
           (simp add: o_assoc comp_fun_commute)
       qed
-      def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
+      define h where "h z = (if z = x then g x - 1 else g z)" for z
       with Suc have "n = h x" by simp
       with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
         by auto