diff -r e9a65675e5e8 -r 8590bf5ef343 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Mon Mar 17 22:34:26 2008 +0100
+++ b/src/HOL/Real/Float.thy	Mon Mar 17 22:34:27 2008 +0100
@@ -114,7 +114,7 @@
 lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
 by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
 
-lemma pow2_int: "pow2 (int c) = (2::real)^c"
+lemma pow2_int: "pow2 (int c) = 2^c"
 by (simp add: pow2_def)
 
 lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
@@ -317,9 +317,6 @@
   then show ?thesis by (simp only: helper)
 qed
 
-lemma pow2_int: "pow2 (int n) = 2^n"
-  by (simp add: pow2_def)
-
 lemma float_add_l0: "float (0, e) + x = x"
   by (simp add: float_def)