--- a/src/HOL/Factorial.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Factorial.thy Wed Jan 10 15:25:09 2018 +0100
@@ -389,13 +389,13 @@
subsection \<open>Misc\<close>
lemma fact_code [code]:
- "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)"
+ "fact n = (of_nat (fold_atLeastAtMost_nat (( * )) 2 n 1) :: 'a::semiring_char_0)"
proof -
have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
by (simp add: fact_prod)
also have "\<Prod>{1..n} = \<Prod>{2..n}"
by (intro prod.mono_neutral_right) auto
- also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
+ also have "\<dots> = fold_atLeastAtMost_nat (( * )) 2 n 1"
by (simp add: prod_atLeastAtMost_code)
finally show ?thesis .
qed