# HG changeset patch
# User nipkow
# Date 1515229691 -3600
# Node ID 9a0bb8e2be07911cf4a3087e5b2b1b64d54a70d6
# Parent  f0f13aa282f49a9a90d051570d6484783dd402bf
tuned op

diff -r f0f13aa282f4 -r 9a0bb8e2be07 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Jan 06 09:39:57 2018 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 06 10:08:11 2018 +0100
@@ -23,7 +23,7 @@
 subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
 
 abbreviation int_ring :: "int ring" ("\<Z>")
-  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
 
 lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
   by simp