
diff -r bdcaa3f3a2f4 -r 339a8b3c4791 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Oct 13 23:02:59 2011 +0200
+++ b/src/HOL/Nitpick.thy	Thu Oct 13 23:27:46 2011 +0200
@@ -63,7 +63,7 @@
 by (auto simp: mem_def)
 
 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
-by simp
+  by (simp only: rtrancl_trancl_reflcl)
 
 lemma rtranclp_unfold [nitpick_unfold, no_atp]:
 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"




