src/HOL/Nitpick_Examples/Manual_Nits.thy

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -115,6 +115,7 @@
 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
 
 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
+unfolding add_raw_def by auto
 
 lemma "add x y = add x x"
 nitpick [show_datatypes, expect = genuine]