# HG changeset patch
# User nipkow
# Date 1515247722 -3600
# Node ID 1f1d85393d70513c3de64c37c1c12377538fea97
# Parent  debef21cbed633371fc01d0f15dfc34d7c1fab71
tuned op

diff -r debef21cbed6 -r 1f1d85393d70 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 06 13:05:25 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 06 15:08:42 2018 +0100
@@ -81,7 +81,7 @@
 nitpick [expect = none]
 oops
 
-lemma "P (op +::nat\<Rightarrow>nat\<Rightarrow>nat)"
+lemma "P ((op +)::nat\<Rightarrow>nat\<Rightarrow>nat)"
 nitpick [card nat = 1, expect = genuine]
 nitpick [card nat = 2, expect = none]
 oops