diff -r a0e6bda62b7b -r 3d51fbf81c17 src/HOL/Integ/IntPower.thy
--- a/src/HOL/Integ/IntPower.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Integ/IntPower.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -12,7 +12,7 @@
   int :: {power}
 
 primrec
-  power_0   "p ^ 0 = #1"
+  power_0   "p ^ 0 = Numeral1"
   power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
 
 end