diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Power.thy
--- a/src/HOL/Power.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Power.thy Mon Apr 25 16:09:26 2016 +0200
@@ -90,7 +90,7 @@
case 0 then show ?case by (simp add: fun_eq_iff)
next
case (Suc n)
- def g \ "\x. f x - 1"
+ define g where "g x = f x - 1" for x
with Suc have "n = g x" by simp
with Suc have "times x ^^ g x = times (x ^ g x)" by simp
moreover from Suc g_def have "f x = g x + 1" by simp