src/HOL/Num.thy

--- a/src/HOL/Num.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Num.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -540,7 +540,7 @@
   by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
 
 lemma numeral_unfold_funpow:
-  "numeral k = (op + 1 ^^ numeral k) 0"
+  "numeral k = ((+) 1 ^^ numeral k) 0"
   unfolding of_nat_def [symmetric] by simp
 
 end