src/HOL/NthRoot.thy

--- a/src/HOL/NthRoot.thy	Sun Oct 19 12:47:34 2014 +0200
+++ b/src/HOL/NthRoot.thy	Sun Oct 19 18:05:26 2014 +0200
@@ -429,8 +429,7 @@
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
 proof -
-  from n obtain m where m: "n = 2 * m"
-    unfolding even_mult_two_ex ..
+  from n obtain m where m: "n = 2 * m" ..
   from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
     by (simp only: power_mult[symmetric] mult.commute)
   then show ?thesis